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