Crafting a Proof Assistant
From MaRDI portal
Publication:3612433
DOI10.1007/978-3-540-74464-1_2zbMATH Open1178.68524DBLPconf/types/AspertiCTZ06OpenAlexW1881760753WikidataQ56901931 ScholiaQ56901931MaRDI QIDQ3612433FDOQ3612433
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
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
- Title not available (Why is that?)
- Proof-assistants using dependent type systems
- An Interactive Driver for Goal-directed Proof Strategies
Uses Software
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)
