TypeTheory

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:

• NaiveComputationalTypeTheory.
• OnUnderstandingTypes
• TheoryOfTypes

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

Several comprehensive books on the subject exist:

• TypesAndProgrammingLanguages and AdvancedTopicsInTypesAndProgrammingLanguages, by BenjaminPierce
• TheoryOfObjects by LucaCardelli and MartinAbadi
• FoundationsOfObjectOrientedProgrammingLanguages by KimBruce
• TypeTheoryAndFunctionalProgramming by SimonThompson (an OnlineBook)

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:

• http://en.wikipedia.org/wiki/Type_theory

TypeSystem

---

CategoryTypeTheory