Editing Type theory (section)

==Applications==
{{Expand section|date=May 2008}}
===Mathematical foundations===
The first computer proof assistant, called [[Automath]], used type theory to encode mathematics on a computer. Martin-Löf specifically developed [[intuitionistic type theory]] to encode ''all'' mathematics to serve as a new foundation for mathematics. There is ongoing research into mathematical foundations using [[homotopy type theory]].

Mathematicians working in [[category theory]] already had difficulty working with the widely accepted foundation of [[Zermelo–Fraenkel set theory]]. This led to proposals such as Lawvere's [[Elementary Theory of the Category of Sets]] (ETCS).<ref>{{nlab|id=ETCS}}</ref> Homotopy type theory continues in this line using type theory. Researchers are exploring connections between dependent types (especially the identity type) and [[algebraic topology]] (specifically [[homotopy]]).

===Proof assistants===
{{main|Proof assistant}}
Much of the current research into type theory is driven by [[Automated proof checking|proof checkers]], interactive [[proof assistant]]s, and [[Automated theorem proving|automated theorem provers]]. Most of these systems use a type theory as the mathematical foundation for encoding proofs, which is not surprising, given the close connection between type theory and programming languages:
* [[Logical framework|LF]] is used by [[Twelf]], often to define other type theories;
* many type theories which fall under [[higher-order logic]] are used by the [[HOL (proof assistant)|HOL family of provers]] and [[Prototype Verification System|PVS]];
* computational type theory is used by [[NuPRL]];
* [[calculus of constructions]] and its derivatives are used by [[Rocq (software)|Rocq]] (previously known as ''Coq''), [[Matita]], and [[Lean (proof assistant)|Lean]];
* UTT (Luo's Unified Theory of dependent Types) is used by [[Agda (programming language)|Agda]] which is both a programming language and proof assistant

Many type theories are supported by [[LEGO (proof assistant)|LEGO]] and [[Isabelle (proof assistant)|Isabelle]]. Isabelle also supports foundations besides type theories, such as [[Zermelo–Fraenkel set theory|ZFC]]. [[Mizar system|Mizar]] is an example of a proof system that only supports set theory.

===Programming languages===
Any [[static program analysis]], such as the type checking algorithms in the [[semantic analysis (compilers)|semantic analysis]] phase of [[compiler]], has a connection to type theory. A prime example is [[Agda (programming language)|Agda]], a programming language which uses UTT (Luo's Unified Theory of dependent Types) for its type system.

The programming language [[ML (programming language)|ML]] was developed for manipulating type theories (see [[Logic for Computable Functions|LCF]]) and its own type system was heavily influenced by them.

===Linguistics===
Type theory is also widely used in [[formal semantics (linguistics)|formal theories of semantics]] of [[natural language]]s,<ref>{{Cite book|last1=Chatzikyriakidis|first1=Stergios|url=https://books.google.com/books?id=iEEUDgAAQBAJ|title=Modern Perspectives in Type-Theoretical Semantics|last2=Luo|first2=Zhaohui|date=2017-02-07|publisher=Springer|isbn=978-3-319-50422-3|language=en|access-date=2022-07-29|archive-date=2023-08-10|archive-url=https://web.archive.org/web/20230810074711/https://books.google.com/books?id=iEEUDgAAQBAJ|url-status=live}}</ref><ref>{{Cite book|last=Winter|first=Yoad|url=https://books.google.com/books?id=aDRWDwAAQBAJ&q=%22formal+semantics%22+%22type+theory%22|title=Elements of Formal Semantics: An Introduction to the Mathematical Theory of Meaning in Natural Language|date=2016-04-08|publisher=Edinburgh University Press|isbn=978-0-7486-7777-1|language=en|access-date=2022-07-29|archive-date=2023-08-10|archive-url=https://web.archive.org/web/20230810074717/https://books.google.com/books?id=aDRWDwAAQBAJ&q=%22formal+semantics%22+%22type+theory%22|url-status=live}}</ref> especially [[Montague grammar]]<ref>Cooper, Robin. "[http://lecomte.al.free.fr/ressources/PARIS8_LSL/ddl-final.pdf Type theory and semantics in flux] {{Webarchive|url=https://web.archive.org/web/20220510190635/http://lecomte.al.free.fr/ressources/PARIS8_LSL/ddl-final.pdf|date=2022-05-10}}." Handbook of the Philosophy of Science 14 (2012): 271-323.</ref> and its descendants. In particular, [[categorial grammar]]s and [[pregroup grammar]]s extensively use type constructors to define the types (''noun'', ''verb'', etc.) of words.

The most common construction takes the basic types <math>e</math> and <math>t</math> for individuals and [[truth-value]]s, respectively, and defines the set of types recursively as follows:
* if <math>a</math> and <math>b</math> are types, then so is <math>\langle a,b\rangle</math>;
* nothing except the basic types, and what can be constructed from them by means of the previous clause are types.

A complex type <math>\langle a,b\rangle</math> is the type of [[Function (mathematics)|functions]] from entities of type <math>a</math> to entities of type <math>b</math>. Thus one has types like <math>\langle e,t\rangle</math> which are interpreted as elements of the set of functions from entities to truth-values, i.e. [[indicator function]]s of sets of entities. An expression of type <math>\langle\langle e,t\rangle,t\rangle</math> is a function from sets of entities to truth-values, i.e. a (indicator function of a) set of sets. This latter type is standardly taken to be the type of [[Generalized quantifier|natural language quantifiers]], like '' everybody'' or ''nobody'' ([[Richard Montague|Montague]] 1973, [[Jon Barwise|Barwise]] and Cooper 1981).<ref>Barwise, Jon; Cooper, Robin (1981) [https://philpapers.org/rec/BARGQA Generalized quantifiers and natural language] ''Linguistics and Philosophy'' '''4''' (2):159--219 (1981)</ref>

[[Type theory with records]] is a [[formal semantics (linguistics)|formal semantics]] representation framework, using ''[[Record_(computer_science)|records]]'' to express ''type theory types''. It has been used in [[natural language processing]], principally [[computational semantics]] and [[dialogue systems]].<ref>{{cite journal|last = Cooper| first = Robin| year = 2005| title = Records and Record Types in Semantic Theory| journal = Journal of Logic and Computation| volume = 15| issue = 2| pages = 99–112| doi = 10.1093/logcom/exi004}}</ref><ref>Cooper, Robin (2010). ''Type theory and semantics in flux''. ''Handbook of the Philosophy of Science. Volume 14: Philosophy of Linguistics''. Elsevier.</ref>

===Social sciences===
[[Gregory Bateson]] introduced a theory of logical types into the social sciences; his notions of [[double bind]] and logical levels are based on Russell's theory of types.