Martin-L–f type theory

Martin-L–f type theory is a constructive, that is, intuitionistic and predicative, theory of sets which is used as a framework for the development of constructive mathematics.

It was developed since the 70s by Martin-L–f and other researchers, in a number of successive variants. The initial aim was to provide a formal system for constructive mathematics but the relevance of the theory also in computer science was soon recognized. In fact, from an intuitionistic perspective, to define a constructive set theory is completely equivalent to define a logical calculus or a language for problem specification, and hence the topic is of immediate relevance both to mathematicians, logicians and computer scientists. Moreover, since an element of a set can also be seen as a proof of the corresponding proposition or as a program which solves the corresponding problem, type theory is also a functional programming language with a very rich type structure and an integrated system to derive correct programs from their specification.

Annotated list of some publications

[Back]