This is an old revision of the document!
Martin-Löf type theory
Meta
A Dependent type theory with Identity type. Or rather it's an umbrella term for several closely related such theories.
Discussion
Reference
Wikipedia: Intuitionistic type theory
Parents
Requirements
