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

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

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.

langue originale	Anglais
titre	Types for Proofs and Programs - International Workshop, TYPES 2006, Revised Selected Papers
Editeur	Springer Verlag
Pages	18-32
Nombre de pages	15
ISBN (imprimé)	9783540744634
Les DOIs	https://doi.org/10.1007/978-3-540-74464-1_2
état	Publié - 1 janv. 2007
Modification externe	Oui
Evénement	International Workshop on Types for Proofs and Programs, TYPES 2006 - Nottingham, Royaume-Uni Durée: 18 avr. 2006 → 21 avr. 2006

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4502 LNCS
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	International Workshop on Types for Proofs and Programs, TYPES 2006
Pays/Territoire	Royaume-Uni
La ville	Nottingham
période	18/04/06 → 21/04/06

Accès au document

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

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

Asperti, A., Coen, C. S., Tassi, E., & Zacchiroli, S. (2007). Crafting a proof assistant. Dans Types for Proofs and Programs - International Workshop, TYPES 2006, Revised Selected Papers (p. 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. Dans 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, p. 18-32, International Workshop on Types for Proofs and Programs, TYPES 2006, Nottingham, Royaume-Uni, 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).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

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 -

Asperti A, Coen CS, Tassi E, Zacchiroli S. Crafting a proof assistant. Dans 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)). doi: 10.1007/978-3-540-74464-1_2

Crafting a proof assistant

Résumé

Série de publications

Une conférence

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation