| Experiences with a mechanisation of Martin-Löf's Theory of Types (1992) | |||||||||||||||||
Abstract | |||||||||||||||||
| Martin-Lof's Theory of Types-MLTT- can be used as a logical framework in which other theories can be defined. This paper describes ILF, a mechanisation of MLTT which allows definition of object theories, judgement checking, reduction of expressions and other facilities for its use. An example of how a particular object theory - Martin-Lof's Monomorphic Theory of Sets - can be defined in ILF and used to develop correct programs is also presented. Keywords : Logical Framework, Programming Logic, Martin-Lof's Theory of Types. Both authors are partially supported by a PEDECIBA (Programa de Desarrollo de las Ciencias B'asicas) grant. 1 Introduction. During the last two decades, as direct result of the strive for the reliability of software there has appeared an increasing interest in methodologies for systematic reasoning about programs. The concept of type, as taken from well known works in foundations of mathematics, has arisen as a very useful tool for dealing with issues connected ... | |||||||||||||||||
Details der Publikation | |||||||||||||||||
| |||||||||||||||||