Type Theory

https://en.wikipedia.org/wiki/Type_theory

Type theory is the study of type systems.

A type system is a formal logical proof system in which every term has a type.

Types define the meaning and operations that can be performed on terms.

Some type theories serve as alternatives to set theory as a foundation of mathematics. Two well-known such theories are Alonzo Church's typed λ-calculus and Per Martin-Löf's intuitionistic type theory.

Type theory was created to avoid paradoxes in previous foundations such as naive set theory, formal logics and rewrite systems.

Type theory is closely related to, and in some cases overlaps with, computational type systems, which are a programming language feature used to reduce bugs.