CentralNotice From Wikipedia, the free encyclopedia Jump to: navigation , search In mathematics , logic , and computer science , a type theory is any of a class of formal systems , some of which can serve as alternatives to set theory as a foundation for all mathematics. In type theory, every "term" has a "type" and operations are restricted to terms of a certain type. Type theory is closely related to (and in some cases overlaps with) type systems , which are a programming language feature used to reduce bugs . The types of type theory were created to avoid paradoxes in a variety of formal logics and rewrite systems and sometimes "type theory" is used to refer to this broader application. Two well-known type theories that can serve as mathematical foundations are Alonzo Church 's typed λ-calculus and Per Martin-Löf 's intuitionistic type theory . 1 History 2 B...