An overview of type theories

TL;DR

This paper provides an overview of pure type systems, focusing on predicative Martin-Löf's intuitionistic type theory and impredicative Coquand's calculus of constructions, highlighting their differences, similarities, and roles in logic and mathematics.

Contribution

It offers a comparative analysis of key type theories, emphasizing their logical foundations and significance in computational science and mathematics.

Findings

Highlights differences between predicative and impredicative type theories

Explores the relationship between type theories and logic

Shows the relevance of type theories in modern mathematics

Abstract

Pure type systems arise as a generalisation of simply typed lambda calculus. The contemporary development of mathematics has renewed the interest in type theories, as they are not just the object of mere historical research, but have an active role in the development of computational science and core mathematics. It is worth exploring some of them in depth, particularly predicative Martin-L\"of's intuitionistic type theory and impredicative Coquand's calculus of constructions. The logical and philosophical differences and similarities between them will be studied, showing the relationship between these type theories and other fields of logic.