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.
Crafting a Proof Assistant / A.Asperti; C.Sacerdoti Coen; E.Tassi; S.Zacchiroli. - STAMPA. - 4502:(2007), pp. 18-32. (Intervento presentato al convegno TYPES 2006 tenutosi a Nottingham, UK nel April 18-21, 2006).
Crafting a Proof Assistant
ASPERTI, ANDREA;SACERDOTI COEN, CLAUDIO;TASSI, ENRICO;
2007
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
