This page is available under URL:

Curriculum Vitae

Date: August 29, 2001
Surname: Bancerek
First name: Grzegorz
Date and place of birth: August 29, 1966; Makowo, Poland
Marital status: Married, 2 children (born 1993, 1996)
Nationality: Polish
Scientific position: Associate Professor, JSPS Postdoctoral Fellow
Affiliation and office address:
Department of Information Engineering
Faculty of Engineering
Shinshu University
380-8553 Japan
Nagano-ken, Nagano-city
Wakasato 4-17-1

Previous affiliation
Institute of Computer Science
Faculty of Mathematics and Physics
University of Bialystok

ul. Akademicka 2
15-267 Bialystok, Poland


Employment: Specialization:
  1. main field - algebraic and categorial aspects of logic
  2. other fields - continuous lattices, computation theory
  3. current research interest - computer aided formalization of mathematics
Project contributions
1. Mizar formalization the theory of continuous lattices
Formalization in Mizar language the theory of continuous lattices according to the book A Compendium of Continuous Lattices by G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. Springer-Verlag, Berlin, Heidelberg, New York, 1980.
Subproject of project 3. started in 1996 and is still continued.
57 Mizar articles written by 15 authors from Poland, Canada, and Japan.
Supported by ONR Grant N00014-95-1-1336, ONR Grant N00014-97-1-0777, NATO Grant CRG 951368, and KBN Grant 8 T11C 018 12.
My contribution: project leader, 19 Mizar articles (including 4 coauthored).
2. Journal of Formalized Mathematics
Automatic text translation/generation from Mizar language into Math English in TeX and HTML form. Resulted programs are used to typeset the journal Formalized Mathematics (ISSN 1426-2630) and its electronic version (URL:
Project started in 1990 and is still developed.
Supported by ONR Grant N00014-95-1-1336 and ONR Grant N00014-97-1-0777.
My contribution: software designer and developer.
3. Mizar Mathematical Library (MML)
MML is a collection of Mizar articles consequently developing mathematical knowledge from Tarski-Grothendieck set theory axioms.
Project started in 1989 and is still developed.
702 articles written by more than 120 authors from 9 countries.
My contribution: 87 articles (including 24 coauthored).
4. Mizar encyclopaedia
Interactive web pages (URL: to browse, search, and analyse the MML. Devoted to aid/support writing Mizar articles.
Project started in 2000.
My contribution: my individual project.
5. Mizar lectures on the Internet
Computer instructions by interactive web pages (URL: to learn Mizar language, system, and the MML. Designed as a part of Shinshu University, Graduate School of Science and Technology on the Internet.
Project started in 2001.
Project is in a state of designing.
My contribution: my individual project.
Computer systems and programming experiences Languages Membership of Professional Societies:
  1. Association of Mizar Users (Stowarzyszenie Uzytkownikow Mizara), member of the Board
  2. American Mathematical Society
  3. Association for Automated Reasoning
  4. Association for Computing Machinery, Polish Chapter
  5. Polish Society of Logic and Philosophy of Sciences (Polskie Towarzystwo Logiczne i Filozofii Nauk)
Awards: Grants: Short visits:


Regular lectures Monographic lectures Seminars Master's students Other university activity

Presentations and publications


List of selected publications:

Continuous lattices
  1. Development of the Theory of Continuous Lattices in Mizar. In M. Kerber and M. Kohlhase, editors, Symbolic Computation and Automated Reasoning, pages 65-80, The CALCULEMUS-2000 Symposium, A.K.Peters, Natick, Massachsetts.
  2. Codifying mathematics. Case study: the theory of continuous lattices. In Volume of Abstracts, 11-th International Congress of Logic, Methodology and Philosophy of Science, Cracow, August 20-26, 1999.
  3. Mizar - a work environment for a mathematician: an experiment with continuous lattices. In Abstracts of Short Communications and Poster Sessions, International Congress of Mathematicians, Berlin, August 18-27, 1998.
  4. Duality based on Galois connection. Part I, Formalized Mathematics, to appear, (URL:
  5. On Characterizations of Compactness, Formalized Mathematics, to appear, (URL:, (coauthors Noboru Endou and Yuji Sakai).
  6. The Characterization of the Continuity of Topologies, Formalized Mathematics, to appear, (URL:, (coauthor Adam Naumowicz).
  7. Lawson Topology and Continuous Lattices, Formalized Mathematics, to appear, (URL:
  8. Prime ideals and filters, Formalized Mathematics, 6(2):241-247, 1997, (URL:
  9. The ``way-below'' relation, Formalized Mathematics, 6(1):169-176, 1997, (URL:
  10. Complete lattices, Formalized Mathematics, 2(5):719-725, 1991, (URL:
Set theory
  1. The mutilated chessboard problem. In R. Matuszewski, editor, The QED Workshop II, Technical Report No. L/1/95, pages 37-38, Warsaw University, Bialystok Branch, 1995.
  2. A model of ZF set theory language. Formalized Mathematics, 1(1):131-145, 1990.
  3. The contraction lemma. Formalized Mathematics, 1(1):201-203, 1990.
  4. The reflection theorem. Formalized Mathematics, 1(5):973-977, 1990.
  5. Universal classes. Formalized Mathematics, 1(3):595-600, 1990. (coauthor Bogdan Nowak)
  6. Zermelo theorem and axiom of choice. Formalized Mathematics, 1(2):265-267, 1990.
  7. Kuratowski - Zorn lemma. Formalized Mathematics, 1(2):387-393, 1990. (coauthor Wojciech A. Trybulec)
  8. König's lemma. Formalized Mathematics, 2(3):397-402, 1991.
Universal algebras
  1. Minimal signature for partial algebra. Formalized Mathematics, 5(3):405-414, 1996.
  2. Translations, endomorphisms, and stable equational theories. Formalized Mathematics, 5(4):553-564, 1996.
  3. Institution of many sorted algebras. Part I: Signature reduct of an algebra. Formalized Mathematics, 6(2):279-287, 1997.
  4. Technical preliminaries to algebraica specifications, Formalized Mathematics, to appear,
  5. Yet another construction of free algebra, Formalized Mathematics, to appear, (coauthor Artur Kornilowicz).
Abstract computers and formal verification
  1. Combining of circuits. Formalized Mathematics, 5(2):283-295, 1996. (coauthor Yatsuka Nakamura)
  2. Full adder circuit. Part I. Formalized Mathematics, 5(3):367-380, 1996. (coauthor Yatsuka Nakamura)
  3. Development of terminology for SCM. Formalized Mathematics, 4(1):61-67, 1993. (coauthor Piotr Rudnicki)
  4. A compiler of arithmetic expressions for SCM. Formalized Mathematics, 5(1):15-20, 1996. (coauthor Piotr Rudnicki)
  5. Circuit generated by terms and circuits calculating terms, Formalized Mathematics, to appear, (URL:
  6. The set of primitive recursive functions, Formalized Mathematics, to appear, (URL:, (coauthor Piotr Rudnicki).
Automated translation
  1. Semi automated translation for mathematics. In J. Darski and Z. Vetulani, editors, Sprache-Kommunikation-Informatik, pages 131-136, Akten des 26. Linguistischen Kolloquiums, Niemeyer, Poznan, 1991. (coauthor Patricia L. Carlson)
Curriculum vitae 1998