Lego projects at LMU Munich

• Bernhard Reus has implemented a version of Snythetic Domain Theory (axiomatizing complete Extensional PERs). The theory can be viewed as a LCF like system where all functions are automatically continuous and formal verification proofs of (recursive) programs can be done. As a case study the Sieve of Eratosthenes has been formally proved using the SDT-logic. To implement SDT in type theory, the Extended Calculus of Constructions was extended by an additional impredicative universe of sets. Correspondingly, also the LEGO-interpreter was subject to minor changes. The change as well as the complete theory and its mathematical background is documented in
  • B. Reus : Synthetic Domain Theory in Type Theory : Another Logic of Computable Functions, accepted for HOTHM, Turku, 1996.
  • B. Reus : Program Verification in Synthetic Domain Theory. Thesis, LMU München, November 1995. Shaker Verlag Aachen.
  • A draft of the above thesis is available via ftp. This thesis contains the development of the theory, the (extended) type theory in use, how the theory is implemented in Lego, a model that ensures that the theory is consistent, and the example proof of the Sieve.
  • The Lego code and a running version of the changed lego system are available by ftp . Note that the code is not executable with the normal Lego-System. The Lego program, about 480 kB, is divided into more than 20 files.