[Constructive Type Theory](https://www.wikiwand.com/en/Intuitionistic_type_theory)/[[Intuitionistic logic|Intuitionistic Type Theory]], often simply called [[Type Theory]], is a framework used in logic, mathematics, and computer science. It emphasizes constructions and the use of types to ensure that mathematical proofs and computations are correct by construction. Here are some key features and principles of Constructive Type Theory: 1. **Constructivism**: In the context of logic and mathematics, constructivism asserts that it is necessary to construct a mathematical object to prove that it exists. This differs from classical logic, where existence can often be proven without constructing the object. Constructive Type Theory typically avoids the law of the excluded middle, which states that any statement is either true or false. 2. **Types**: Types are central to Type Theory. Every term or expression in Type Theory has a type, which serves as a sort of label that governs how the term can be used. Types can represent simple sets, propositions, functions, or more complex structures. By using types, Type Theory ensures that only sensible operations are performed (e.g., adding two numbers, but not adding a number and a string). 3. **Propositions as Types**: A key idea in Type Theory is the correspondence between propositions and types. A proposition is identified with the type of its proofs. If a proposition is true, there exists a term of its corresponding type (i.e., a proof of the proposition). This is known as the [[Curry-Howard correspondence]], which forms a bridge between computational and logical aspects of mathematics. See [[@PropositionsTypesComputerphile2017]] 4. **Dependent Types**: These are types that depend on values. Dependent types allow expressions where the type of a variable can depend on the value of another variable. This capability enhances the expressiveness of Type Theory, enabling it to specify and verify richer properties in a system. 5. **Intuitionistic Logic**: Type Theory typically uses intuitionistic logic, which is constructive logic that does not accept the law of excluded middle as a general principle. In intuitionistic logic, a proof of a proposition's negation is not merely a disproof of the proposition but a construction of a proof of its falsehood. 6. **Applications**: Constructive Type Theory has found applications in several areas. It is foundational in the design of proof assistants like Coq, Agda, and Lean, which are tools used to formalize mathematics and verify software and hardware correctness. It also influences functional programming languages like Haskell and ML, where types play a crucial role in ensuring program correctness. This theory has been developed by various logicians and mathematicians, but one of the notable figures is Per Martin-Löf, whose work on Intuitionistic Type Theory has been particularly influential. # References ```dataview Table title as Title, authors as Authors where contains(subject, "type theory") sort title, authors, modified ```