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:

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

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:

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