On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory

DOI10.1007/978-3-540-78969-7_2zbMATH Open1137.68570OpenAlexW4235247099MaRDI QIDQ5458424FDOQ5458424

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

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

Mathematics Subject Classification ID

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

Cited In (10)

• 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
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)

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)