Type theory

The topic of type theory is fundamental both in logic and computer Science , for instance:

1. Reynolds 1983 and 1985.
2. Paradoxes and Russell's Type Theories
3. Simple Type Theory and the λ -Calculus.

Church's type theory, aka simple type theory, is a formal logical language which includes classical first-order and propositional logic, but is more expressive in a practical sense. It is used, with some modifications and enhancements, in most modern applications of type theory.