Lehr- und Forschungseinheit für
Programmierung und Softwaretechnik,
Institut für Informatik der Ludwig-Maximilians-Universität München
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.
Bernhard Reus
(9.07.1996)