Definition
Martin-Löf Type Theory (MLTT) is an Intuitionism, predicative dependent type theory introduced by Per Martin-Löf.
Abstract
MLTT designates the family of type theories derived from the foundational work of Per Martin-Löf. It integrates logic and computation through the propositions-as-types correspondence, functioning as the basis for modern dependently typed languages and proof assistants.
The Logical Framework
The presentation of MLTT is frequently mediated by a core Logical Framework. The base framework contains dependent function types (-types) and a few structural constructs. We formulate extensions to the base system by introducing new type formers as constants reflecting into a Tarski universe . This isolates the generic machinery of binding and substitution from the specific rules of individual type formers.
Inductive Types and Pattern Matching
Implementations utilizing the Logical Framework, notably the Alf system, permit the definition of types within a universe simply by declaring their constructors. We then construct functions over these inductive types via dependent pattern matching on the constructors, rather than relying exclusively on primitive recursors or elimination constants.