Type Theory

The theory behind type systems used for programming languages and other kinds of formal languages. The discipline is a branch and receives influences from other mathematical disciplines like Mathematical Logic, ProgrammingLanguageTheory, CategoryTheory, ProofTheory, etc.

Some good introductions available on the web are:

NCTT is a bit more technical; OUT is a bit easier for laypersons to grasp.

Several comprehensive books on the subject exist:

In addition, BenjaminPierce maintains an excellent bibliography on the topic at http://www.cis.upenn.edu/~bcpierce/courses/670Fall04/GreatWorksInPL.shtml.

The website LambdaTheUltimate (whose topic is programming language theory) contains lots of interesting material on TypeTheory; it's one of the most widely-discussed topics there.


ThreadMess discussion moved to TopsTypeTheoryDiscussion


Related:

TypeSystem


CategoryTypeTheory


EditText of this page (last edited May 17, 2013) or FindPage with title or text search