Crafting a proof assistant

Andrea Asperti; Claudio Sacerdoti Coen; Enrico Tassi; Stefano Zacchiroli

doi:10.1007/978-3-540-74464-1_2

Crafting a proof assistant

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

University of Bologna

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

Proof assistants are complex applications whose development has never been properly systematized or documented. This work is a contribution in this direction, based on our experience with the development of Matita: a new interactive theorem prover based - as Coq - on the Calculus of Inductive Constructions (CIC). In particular, we analyze its architecture focusing on the dependencies of its components, how they implement the main functionalities, and their degree of reusability. The work is a first attempt to provide a ground for a more direct comparison between different systems and to highlight the common functionalities, not only in view of reusability but also to encourage a more systematic comparison of different softwares and architectural solutions.

Original language	English
Title of host publication	Types for Proofs and Programs - International Workshop, TYPES 2006, Revised Selected Papers
Publisher	Springer Verlag
Pages	18-32
Number of pages	15
ISBN (Print)	9783540744634
DOIs	https://doi.org/10.1007/978-3-540-74464-1_2
Publication status	Published - 1 Jan 2007
Externally published	Yes
Event	International Workshop on Types for Proofs and Programs, TYPES 2006 - Nottingham, United Kingdom Duration: 18 Apr 2006 → 21 Apr 2006

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4502 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Workshop on Types for Proofs and Programs, TYPES 2006
Country/Territory	United Kingdom
City	Nottingham
Period	18/04/06 → 21/04/06

Access to Document

10.1007/978-3-540-74464-1_2

Cite this

Asperti, A., Coen, C. S., Tassi, E., & Zacchiroli, S. (2007). Crafting a proof assistant. In Types for Proofs and Programs - International Workshop, TYPES 2006, Revised Selected Papers (pp. 18-32). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4502 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-540-74464-1_2

@inproceedings{5e0188f9c15e4ce98b2a583417cd4293,

title = "Crafting a proof assistant",

abstract = "Proof assistants are complex applications whose development has never been properly systematized or documented. This work is a contribution in this direction, based on our experience with the development of Matita: a new interactive theorem prover based - as Coq - on the Calculus of Inductive Constructions (CIC). In particular, we analyze its architecture focusing on the dependencies of its components, how they implement the main functionalities, and their degree of reusability. The work is a first attempt to provide a ground for a more direct comparison between different systems and to highlight the common functionalities, not only in view of reusability but also to encourage a more systematic comparison of different softwares and architectural solutions.",

author = "Andrea Asperti and Coen, \{Claudio Sacerdoti\} and Enrico Tassi and Stefano Zacchiroli",

year = "2007",

month = jan,

day = "1",

doi = "10.1007/978-3-540-74464-1\_2",

language = "English",

isbn = "9783540744634",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "18--32",

booktitle = "Types for Proofs and Programs - International Workshop, TYPES 2006, Revised Selected Papers",

note = "International Workshop on Types for Proofs and Programs, TYPES 2006 ; Conference date: 18-04-2006 Through 21-04-2006",

}

Asperti, A, Coen, CS, Tassi, E & Zacchiroli, S 2007, Crafting a proof assistant. in Types for Proofs and Programs - International Workshop, TYPES 2006, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4502 LNCS, Springer Verlag, pp. 18-32, International Workshop on Types for Proofs and Programs, TYPES 2006, Nottingham, United Kingdom, 18/04/06. https://doi.org/10.1007/978-3-540-74464-1_2

Crafting a proof assistant. / Asperti, Andrea; Coen, Claudio Sacerdoti; Tassi, Enrico et al.
Types for Proofs and Programs - International Workshop, TYPES 2006, Revised Selected Papers. Springer Verlag, 2007. p. 18-32 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4502 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Crafting a proof assistant

AU - Asperti, Andrea

AU - Coen, Claudio Sacerdoti

AU - Tassi, Enrico

AU - Zacchiroli, Stefano

PY - 2007/1/1

Y1 - 2007/1/1

N2 - Proof assistants are complex applications whose development has never been properly systematized or documented. This work is a contribution in this direction, based on our experience with the development of Matita: a new interactive theorem prover based - as Coq - on the Calculus of Inductive Constructions (CIC). In particular, we analyze its architecture focusing on the dependencies of its components, how they implement the main functionalities, and their degree of reusability. The work is a first attempt to provide a ground for a more direct comparison between different systems and to highlight the common functionalities, not only in view of reusability but also to encourage a more systematic comparison of different softwares and architectural solutions.

AB - Proof assistants are complex applications whose development has never been properly systematized or documented. This work is a contribution in this direction, based on our experience with the development of Matita: a new interactive theorem prover based - as Coq - on the Calculus of Inductive Constructions (CIC). In particular, we analyze its architecture focusing on the dependencies of its components, how they implement the main functionalities, and their degree of reusability. The work is a first attempt to provide a ground for a more direct comparison between different systems and to highlight the common functionalities, not only in view of reusability but also to encourage a more systematic comparison of different softwares and architectural solutions.

UR - https://www.scopus.com/pages/publications/38049126096

U2 - 10.1007/978-3-540-74464-1_2

DO - 10.1007/978-3-540-74464-1_2

M3 - Conference contribution

AN - SCOPUS:38049126096

SN - 9783540744634

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 18

EP - 32

BT - Types for Proofs and Programs - International Workshop, TYPES 2006, Revised Selected Papers

PB - Springer Verlag

T2 - International Workshop on Types for Proofs and Programs, TYPES 2006

Y2 - 18 April 2006 through 21 April 2006

ER -

Crafting a proof assistant

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this