Editing Type theory (section)

==Further reading==
{{refbegin}}
* {{cite web|first1=C.|last1=Aarts|first2=R.|last2=Backhouse|first3=P.|last3=Hoogendijk|first4=E.|last4=Voermans|first5=J.|last5=van der Woude|title=A Relational Theory of Datatypes|date=December 1992|publisher=Technische Universiteit Eindhoven|url=https://www.researchgate.net/publication/277287583}}
* {{cite book|first=Peter|last=Andrews B.|year=2002|isbn=978-1-4020-0763-7|title=An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof|edition=2nd|publisher=Kluwer}}
*{{cite book|first=Bart|last=Jacobs|title=Categorical Logic and Type Theory|year=1999|publisher=Elsevier|isbn=978-0-444-50170-7|series=Studies in Logic and the Foundations of Mathematics|volume=141|url=https://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html|access-date=2020-07-19|archive-date=2023-08-10|archive-url=https://web.archive.org/web/20230810075226/https://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html|url-status=live}} Covers type theory in depth, including polymorphic and dependent type extensions. Gives [[categorical semantics]].
* {{cite book|first=Luca|last=Cardelli|chapter=Type Systems|chapter-url=http://citeseer.ist.psu.edu/cardelli97type.html|editor-first=Allen B.|editor-last=Tucker|title=The Computer Science and Engineering Handbook|publisher=CRC Press|year=1996|isbn=9780849329098|pages=2208–36|access-date=2004-06-26|archive-date=2008-04-10|archive-url=https://web.archive.org/web/20080410185229/http://citeseer.ist.psu.edu/cardelli97type.html|url-status=live}}
* {{cite book|first=Jordan E.|last=Collins|year=2012|isbn=978-3-8473-2963-3|title=A History of the Theory of Types: Developments After the Second Edition of 'Principia Mathematica'|publisher=Lambert Academic Publishing|hdl=11375/12315}} Provides a historical survey of the developments of the theory of types with a focus on the decline of the theory as a foundation of mathematics over the four decades following the publication of the second edition of 'Principia Mathematica'.
* {{cite book|author-link=Robert Lee Constable|last=Constable|first=Robert L.|chapter=Naïve Computational Type Theory|chapter-url=http://www.nuprl.org/documents/Constable/naive.pdf|archive-url=https://ghostarchive.org/archive/20221009/http://www.nuprl.org/documents/Constable/naive.pdf|archive-date=2022-10-09|url-status=live|editor-first=H.|editor-last=Schwichtenberg|editor-first2=R.|editor-last2=Steinbruggen|title=Proof and System-Reliability|publisher=Springer|series=Nato Science Series II|volume=62|year=2012|orig-year=2002|isbn=9789401004138|pages=213–259}} Intended as a type theory counterpart of [[Paul Halmos]]'s (1960) ''[[Naive Set Theory (book)|Naïve Set Theory]]''
* {{cite encyclopedia|author-link=Thierry Coquand|first=Thierry|last=Coquand|title=Type Theory|date=2018|orig-year=2006|encyclopedia=[[Stanford Encyclopedia of Philosophy]]|url=http://plato.stanford.edu/entries/type-theory/}}
* {{cite book|first=Simon|last=Thompson|title=Type Theory and Functional Programming|publisher=Addison–Wesley|year=1991|isbn=0-201-41667-0|url=http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/|access-date=2006-04-03|archive-date=2021-03-23|archive-url=https://web.archive.org/web/20210323203228/http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/|url-status=live}}
* {{cite book|author-link=J. Roger Hindley|first=J. Roger|last=Hindley|title=Basic Simple Type Theory|publisher=Cambridge University Press|year=2008|orig-year=1995|isbn=978-0-521-05422-5}}<!--no idea why these get different ISBNs, they don't appear to be different editions--> A good introduction to simple type theory for computer scientists; the system described is not exactly Church's STT though. [http://www.iwu.edu/~htiede/papers/pdf/jolli-review.pdf Book review] {{Webarchive|url=https://web.archive.org/web/20110607234927/http://www.iwu.edu/~htiede/papers/pdf/jolli-review.pdf|date=2011-06-07}}
* {{cite book|first1=Fairouz D.|last1=Kamareddine|first2=Twan|last2=Laan|first3=Rob P.|last3=Nederpelt|title=A modern perspective on type theory: from its origins until today|publisher=Springer|year=2004|isbn=1-4020-2334-0}}
* {{cite book|first1=José|last1=Ferreirós|first2=José Ferreirós|last2=Domínguez|title=Labyrinth of thought: a history of set theory and its role in modern mathematics|publisher=Springer|year=2007|isbn=978-3-7643-8349-7|edition=2nd|chapter=X. Logic and Type Theory in the Interwar Period}}
* {{cite thesis|first=T.D.L.|last=Laan|title=The evolution of type theory in logic and mathematics|date=1997|type=PhD|publisher=Eindhoven University of Technology|url=https://pure.tue.nl/ws/files/1383309/498552.pdf|archive-url=https://ghostarchive.org/archive/20221009/https://pure.tue.nl/ws/files/1383309/498552.pdf|archive-date=2022-10-09|url-status=live|doi=10.6100/IR498552|isbn=90-386-0531-5}}
* Montague, R. (1973) "The proper treatment of quantification in ordinary English". In K. J. J. Hintikka, J. M. E. Moravcsik, and P. Suppes (eds.), ''Approaches to Natural Language'' (Synthese Library, 49), Dordrecht: Reidel, 221–242; reprinted in Portner and Partee (eds.) 2002, pp. 17–35. See: [https://plato.stanford.edu/entries/montague-semantics/#Bib Montague Semantics], Stanford Encyclopedia of Philosophy.''
{{refend}}