Type theory is a formal language which can be used as a programming
language [1] and also as a foundation for mathematics [2] replacing
first order logic and set theory. Its current form was described by
Per Martin-Löf in the 1970s [1]. There are several computer
implementations of type theory (also called proof assistants), the
most popular ones are Agda, Coq, Idris, Lean. These are functional
programming languages close in spirit to Haskell, ML, F#. Type theory
can be seen as an algebraic theory [3] (such as rings or vector
spaces), its important properties such as parametricity and canonicity
[4] can be proved algebraically. Interesting research areas include
the following.
- Efficient computer implementation of type theory. Lambda calculus,
type checking, elaboration, normalisation. See [5]
- Inductive and coinductive types in type theory. How to specify and
implement them? The syntax of type theory itself is an inductive
type. Turing machinges are coinductive. See [6,7]
- A type theory with function extensionality. How to prove its
metatheoretic properties? See [8] for a start.
The topic is very technical, it involves lots of syntactic
manipulation. Some people like to overcome this by computer-checking
every argument using proof assistants. Other people like to make it
very abstract using category theory [9].