[[Martin-Löf Type Theory]] ([[MLTT]]) is a formal system for constructive mathematics and computer programming. It was developed by the Swedish mathematician and philosopher Per Martin-Löf in the 1970s as an alternative to set theory and classical logic. # A 30 minute Primer It would be very helpful to watch this 30 minute video on Martin-Löf Type Theory:  At its core, MLTT is based on the idea that types represent propositions or statements, and that objects of these types represent proofs or evidence for these propositions. In MLTT, types are seen as a fundamental concept that can be used to reason about both mathematical objects and computer programs. # MLTT and Polynomial Functor [[MLTT]] introduces several key concepts, including dependent types, which allow types to depend on values or other types. This enables precise specifications of properties of objects and functions. MLTT also includes a rich system of type constructors, such as product types (representing conjunction), sum types (representing disjunction), function types (representing implication), and dependent function types (representing universal quantification). They help construct the notion of [[Polynomial functor]]. One important feature of MLTT is its constructive nature. This means that every proof or evidence must be algorithmically constructible, providing a basis for computer programs as well. This differs from classical logic where proofs can be non-constructive. # Linear Logic and MLTT There are several connections between [[Linear Logic]] and [[Martin-Löf Type Theory]] (MLTT), which are two prominent formal systems in the field of logic and computer science. 1. Semantics: Both Linear Logic and MLTT have a strong connection to their respective semantics. Linear Logic is closely tied to the notion of resource management, where propositions represent resources that can be used and consumed. MLTT is based on constructive type theory, where types represent propositions and terms represent proofs or evidence for those propositions. 2. Curry-Howard correspondence: Both Linear Logic and MLTT have a correspondence between logical inference rules and computational operations. This correspondence is known as the Curry-Howard correspondence. In MLTT, types correspond to logical propositions, terms correspond to proofs, and the process of constructing or checking a proof corresponds to computation. Similarly, in Linear Logic, the various connectives and inference rules correspond to computational operations. 3. Dependent types: MLTT allows for the definition of dependent types, where types can depend on values or other types. This feature allows for precise specification of properties about programs or proofs. Linear Logic also supports dependent types through the use of linear function spaces, where functions can have linear dependencies on their inputs. 4. Substructural nature: Both Linear Logic and MLTT are substructural logics, meaning that they relax some of the structural rules present in classical logic. In Linear Logic, this is manifested through its resource-oriented approach with different modalities (e.g., linear implication) that control how resources are used or consumed. MLTT relaxes some structural rules through its constructive approach to logic, allowing for more flexible reasoning about dependent types. 5. Computational interpretation: Both Linear Logic and MLTT have been used as foundations for programming languages with strong computational capabilities. For example, linear type systems inspired by Linear Logic have been used in programming languages like [[Rust]] to enforce memory safety guarantees. Similarly, MLTT has influenced languages like [[Agda]] and [[Coq]], which provide powerful theorem proving capabilities. Overall, while Linear Logic and MLTT have different origins and motivations, they share several connections in terms of their semantics, computational interpretation, and foundational aspects. These connections have led to fruitful interactions between the two formal systems in areas such as proof theory, type theory, and programming languages. # Conclusion MLTT has found applications in various areas including formal verification of software and hardware systems, proof assistants like [[Coq]] and [[Agda]], as well as foundations of mathematics. It has also influenced other type theories like [[Homotopy Type Theory]], which connects type theory with abstract homotopy theory in topology. # References ```dataview Table title as Title, authors as Authors where contains(subject, "Martin-Löf Type Theory") or contains(subject, "MLTT") or contains(title, "Martin-Löf Type Theory") or contains(title, "MLTT") ```