Editing Type theory (section)

==External links==

===Introductory material===
*[https://ncatlab.org/nlab/show/type+theory Type Theory at nLab], which has articles on many topics.
*[https://plato.stanford.edu/entries/type-theory-intuitionistic/ Intuitionistic Type Theory] article at the Stanford Encyclopedia of Philosophy
*[https://home.ttic.edu/~dreyer/course/papers/barendregt.pdf Lambda Calculi with Types] book by Henk Barendregt
*[https://hbr.github.io/Lambda-Calculus/cc-tex Calculus of Constructions / Typed Lambda Calculus] textbook style paper by Helmut Brandl
*[https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf Intuitionistic Type Theory] notes by Per Martin-Löf
*[https://www.cse.chalmers.se/research/group/logic/book/book.pdf Programming in Martin-Löf's Type Theory] book
*[https://homotopytypetheory.org/book/ Homotopy Type Theory] book, which proposed homotopy type theory as a mathematical foundation.

===Advanced material===
* {{scholarpedia|title=Computational type theory|urlname=Computational_type_theory|curator=Robert L. Constable}}
* [http://lists.seas.upenn.edu/mailman/listinfo/types-list The TYPES Forum] &mdash; moderated e-mail forum focusing on type theory in computer science, operating since 1987.
* [ftp://ftp.cs.cornell.edu/pub/nuprl/doc/book.ps.gz The Nuprl Book]: "Introduction to Type Theory."
* [http://www.cs.chalmers.se/Cs/Research/Logic/Types/tutorials.html Types Project lecture notes] of summer schools 2005–2008
** The [http://www.cs.chalmers.se/Cs/Research/Logic/TypesSS05/program.html 2005 summer school] has introductory lectures
*[https://www.cs.uoregon.edu/research/summerschool/archives.html Oregon Programming Languages Summer School], many lectures and some notes.
**[https://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html Summer 2013 lectures] including [https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_YncjXRzdGq2SjKv5F2J8HUFeqN Robert Harper's talks on YouTube]
**[https://www.cs.uoregon.edu/research/summerschool/summer15/curriculum.html Summer 2015 Types, Logic, Semantics, and Verification]
* [http://math.andrej.com/category/type-theory/ Andrej Bauer's blog]

{{Computer science}}
{{Mathematical logic}}
{{Formal semantics}}

{{DEFAULTSORT:Type Theory}}
[[Category:Type theory| ]]
[[Category:Systems of formal logic]]
[[Category:Hierarchy]]