Crafting a Proof Assistant
From MaRDI portal
Publication:3612433
DOI10.1007/978-3-540-74464-1_2zbMath1178.68524OpenAlexW1881760753WikidataQ56901931 ScholiaQ56901931MaRDI QIDQ3612433
Andrea Asperti, Stefano Zacchiroli, Claudio Sacerdoti Coen, Enrico Tassi
Publication date: 10 March 2009
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-74464-1_2
Related Items
Classification of alignments between concepts of formal mathematical systems, Functions-as-constructors higher-order unification: extended pattern unification, A scalable module system, Formal metatheory of programming languages in the Matita interactive theorem prover, A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading, Representing model theory in a type-theoretical logical framework, An Interactive Driver for Goal-directed Proof Strategies, The proof monad, Experiences from exporting major proof assistant libraries, A compact kernel for the calculus of inductive constructions, The future of logic: foundation-independence
Uses Software
