Crafting a Proof Assistant

DOI10.1007/978-3-540-74464-1_2MaRDI QIDQ3612433zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli

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

Mathematics Subject Classification ID

Recommendations

• User interaction with the Matita proof assistant
• Proof-assistants using dependent type systems
• scientific article; zbMATH DE number 1629953
• Web interfaces for proof assistants
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.

Cited in

(14)

• The future of logic: foundation-independence
• User interaction with the Matita proof assistant
• A scalable module system
• Representing model theory in a type-theoretical logical framework
• The proof monad
• Functions-as-constructors higher-order unification: extended pattern unification
• Classification of alignments between concepts of formal mathematical systems
• A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
• A compact kernel for the calculus of inductive constructions
• Formal metatheory of programming languages in the Matita interactive theorem prover
• Experiences from exporting major proof assistant libraries
• scientific article; zbMATH DE number 3874584 (Why is no real title available?)
• Proof-assistants using dependent type systems
• An Interactive Driver for Goal-directed Proof Strategies

Describes a project that uses

Uses Software

• CtCoq
• ALF
• Matita
• Proof General
• Coq

This page was built for publication: Crafting a Proof Assistant

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