Contents

# 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.

Last revised on January 12, 2014 at 10:12:06. See the history of this page for a list of all contributions to it.