On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
From MaRDI portal
Publication:5458424
DOI10.1007/978-3-540-78969-7_2zbMath1137.68570OpenAlexW4235247099MaRDI QIDQ5458424
Thierry Coquand, Andreas Abel, 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
Categorical logic, topoi (03G30) Cut-elimination and normal-form theorems (03F05) Second- and higher-order arithmetic and fragments (03F35)
Related Items
Kripke models for classical logic, The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective, Dependent Types at Work, Unnamed Item, A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance