On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory

DOI10.1007/978-3-540-78969-7_2MaRDI QIDQ5458424zbMATH OpenOpenAlexFDO

Authors Andreas Abel, Thierry Coquand, Peter Dybjer

Publication date 11 April 2008

Published in Functional and Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78969-7_2

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Categorical logic, topoi (03G30) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• Algebra of constructions II: an algebraic approach to Martin-Löf type theory and the calculus of constructions
• A type theoretic interpretation of constructive domain theory
• Categorical and algebraic aspects of Martin-Löf type theory
• scientific article; zbMATH DE number 1187955
• AN INTERPRETATION OF MARTIN‐LÖF'S CONSTRUCTIVE THEORY OF TYPES IN ELEMENTARY TOPOS THEORY

Cited in

(10)

• scientific article; zbMATH DE number 65534 (Why is no real title available?)
• Dependent Types at Work
• The interpretation of intuitionistic type theory in locally Cartesian closed categories -- an intuitionistic perspective
• Fiat: deductive synthesis of abstract data types in a proof assistant
• Categorical and algebraic aspects of Martin-Löf type theory
• Kripke models for classical logic
• scientific article; zbMATH DE number 7559297 (Why is no real title available?)
• A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
• Working with Mathematical Structures in Type Theory
• An algorithm for checking incomplete proof objects in type theory with localization and unification

This page was built for publication: On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5458424)