Type theory is a branch of mathematical logic and theoretical computer science in which every term has an associated type, and well-formedness is governed by typing rules rather than by raw set membership. It serves both as a foundation for mathematics and as the formal basis for type systems in programming languages, where types constrain valid expressions. Through the propositions-as-types correspondence, proofs become programs and types become specifications, linking logic, computation and formal verification.
Overview
- Type theory arose partly to avoid paradoxes in naive set theory by stratifying mathematical objects into types.
- Simply typed and polymorphic lambda calculi, intuitionistic type theory and dependent type theory form a progression of increasingly expressive systems.
- The Curry-Howard correspondence equates propositions with types and proofs with programs, so a type checker can act as a proof checker.
- Modern dependently typed languages and proof assistants exploit this to mechanise mathematics and verify software against rich specifications.
Key aspects
- Terms, types and the judgements that relate them.
- Typing rules and the inference of types for expressions.
- Polymorphism, abstraction and parametricity.
- Dependent types where types may depend on values.
- The correspondence between logical propositions and types.
Mechanisms
- Type-checking algorithms that validate or reject expressions.
- Type inference reconstructing omitted type annotations.
- Reduction and normalisation of typed terms.
- Encoding of logical connectives as type constructors.
- Elaboration of high-level surface syntax into core typed terms.
Applications
- Foundations of statically typed programming languages.
- Proof assistants and mechanised mathematics.
- Verified compilers and safety-critical software.
- Specification and formal verification of algorithms and protocols.
- Reasoning about program correctness and security properties.