View source for Type theory

In [[mathematics]], [[logic]], and [[computer science]], a '''type theory''' is any of a class of [[Formal system|formal systems]], some of which can serve as alternatives to [[set theory]] as a foundation for all mathematics.

== Description ==

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 system|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 logic|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.

== See also ==

* [[Data type]] for concrete types of data in programming
* [[Domain theory]]
* [[Type (model theory)]]
* [[Type system]] for a more practical discussion of type systems for programming languages

== External links ==

* [https://en.wikipedia.org/wiki/Type_theory Type theory] @ Wikipedia.org 

[[Category:Computer science]]
[[Category:Logic]]
[[Category:Mathematics]]