[Revised entry by Peter Dybjer and Erik Palmgren on September 23, 2024.
Changes to: Main text, Bibliography]
Intuitionistic type theory (also constructive type theory or Martin-Lof type theory) is a formal logical system and philosophical foundation for constructive mathematics. It is a full-scale system which aims to play a similar role for constructive mathematics as Zermelo-Fraenkel Set Theory does for classical mathematics. It is based on the…
Read the full article which is published on Stanford Encyclopedia of Philosophy (external link)