Formal Development of Functional Programs in Type Theory - A Case Study

Martin Hofmann

Abstract: Type systems like the Extended Calculus of Constructions (ECC) [Luo 90] have been proposed as an environment in which to develop both modular programs and their correctness proofs. This work describes a case study in this area which uses the implementation Lego by R Pollack of the ECC. After introducing the main concepts of type-theoretic specification and verification we describe a machine-checked version of the symbol table example given in [Sannella 89]. Particular attention is paid to a detailed description of the actual interaction with Lego as a program development system, so as to provide a basis for further research on this topic. The case study is a shortened version of the author's Diplomarbeit (Master's thesis).

LFCS report ECS-LFCS-92-228

Previous | Index | Next