
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Computability, Logic, AI Algorithms
