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