An overview of type theories
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.
Keywords
Cite
@article{arxiv.1411.1029,
title = {An overview of type theories},
author = {Nino Guallart},
journal= {arXiv preprint arXiv:1411.1029},
year = {2014}
}
Comments
Conference: Philosophy of Science in the 21st Century: Challenges and Tasks, Faculdade de Ci\^encias da Universidade de Lisboa (Portugal), December 2013