# Contents

## Idea

In type theory, regarding propositions as types, a proof of a proposition is given by constructing a term of the corresponding type. This can hence be regarded as a program to compute a specific term (output).

## References

An exposition is in

That Martin-Löf dependent type theory can be regarded also as a functional programming language by identifying proofs as programs was stressed in

• Per Martin-Löf, Constructive mathematics and computer programming, Philosophical Transactions of the Royal Society of London (Series A) 312 (1984), no. 1522, pp. 501–518.

Revised on January 12, 2014 10:12:06 by Urs Schreiber (89.204.137.148)