|
 
|
[Del10] Assisting Users of Proof Assistants
Mémoire de HDR : Soutenue le: 09 December 2010, pp.: Directeur:Rapporteur 1:
Rapporteur 2:
Membre du jury:
Membre du jury:
Membre du jury:,
motcle:
Résumé:
This document proposes to present the results of more than ten years of research by the author, which aim to improve several techniques related to theorem proving. These improvements are guided by the following leitmotiv: how to make theorem proving easier to use? This work starts from the self-evident fact that theorem proving represents actually a very thin part of the spectrum of formal methods, especially compared to model checking. Automation is probably one of the main causes, but some other reasons may also be found elsewhere, such as in the way of building specifications or interacting with theorem provers. Thus, this document is organized around these three topics, that are structuring, automating, and communicating.
The first part of this document focuses on the specification languages involved in theorem provers. In particular, we make use of the Focal language, which allows us to build certified applications. To understand how the design features of Focal can be appropriate in practice, a significant application, realized in the framework of the EDEMOI project, is described, and which consists of the formalization of airport security regulations in the domain of civil aviation. In the idea of clearly identifying specifications and implementations, we present, in the context of the Coq proof assistant, another work which aims to execute inductive relations. Finally, we discuss the notion of reuse with an experiment, which consists in retrieving information, typically theorems, in a proof library using types as keys and up to isomorphisms.
The second part of this document is devoted to automation in theorem proving. First, the problem is handled in terms of power of automation, introducing a proof dedicated meta-language, which is intended to tailor automation in the framework of Coq. Next, we describe several experiments which aim to import computations from computer algebra systems into proof assistants in a pure skeptical way (i.e. verifying the soundness of the computations). Among these experiments, some interfaces have been realized between Coq and Maple, as well as between Focal and Axiom. Lastly, in the same idea of skeptical computations, we propose to adapt this idea to automated deduction with two contributions related to the Zenon automated theorem prover. These contributions respectively consist in verifying the proofs produced by Zenon by generating Coq proofs, and validating supplementary rules involved in applications developed using the B method by means of Zenon proofs.
In the third part of this document, we aim to draw attention to several means of communicating with theorem provers. Regarding the input language and in the framework of Coq, we propose a language designed to describe proofs and intended to be style-independent. Concerning the output language, we present a transformation from Focal specifications to UML models, which is an appropriate means of producing comprehensible documents for end-users, such as the certification authorities in the context of the EDEDMOI project. Finally, still considering output languages, we introduce a scheme of compilation for Focal, which is based on the notion of modules and allows us to get traceability between Focal specifications and compiled codes.
The first part of this document focuses on the specification languages involved in theorem provers. In particular, we make use of the Focal language, which allows us to build certified applications. To understand how the design features of Focal can be appropriate in practice, a significant application, realized in the framework of the EDEMOI project, is described, and which consists of the formalization of airport security regulations in the domain of civil aviation. In the idea of clearly identifying specifications and implementations, we present, in the context of the Coq proof assistant, another work which aims to execute inductive relations. Finally, we discuss the notion of reuse with an experiment, which consists in retrieving information, typically theorems, in a proof library using types as keys and up to isomorphisms.
The second part of this document is devoted to automation in theorem proving. First, the problem is handled in terms of power of automation, introducing a proof dedicated meta-language, which is intended to tailor automation in the framework of Coq. Next, we describe several experiments which aim to import computations from computer algebra systems into proof assistants in a pure skeptical way (i.e. verifying the soundness of the computations). Among these experiments, some interfaces have been realized between Coq and Maple, as well as between Focal and Axiom. Lastly, in the same idea of skeptical computations, we propose to adapt this idea to automated deduction with two contributions related to the Zenon automated theorem prover. These contributions respectively consist in verifying the proofs produced by Zenon by generating Coq proofs, and validating supplementary rules involved in applications developed using the B method by means of Zenon proofs.
In the third part of this document, we aim to draw attention to several means of communicating with theorem provers. Regarding the input language and in the framework of Coq, we propose a language designed to describe proofs and intended to be style-independent. Concerning the output language, we present a transformation from Focal specifications to UML models, which is an appropriate means of producing comprehensible documents for end-users, such as the certification authorities in the context of the EDEDMOI project. Finally, still considering output languages, we introduce a scheme of compilation for Focal, which is based on the notion of modules and allows us to get traceability between Focal specifications and compiled codes.
Equipe:
sys
BibTeX
| @misc { | |||
| Del10, | |||
| title | = | "{Assisting Users of Proof Assistants}", | |
| author | = | "D. Delahaye", | |
| year | = | 2010, | |
| address | = | "{CEDRIC Laboratory, Paris, France}", | |
| note | = | "{Post-Doctoral Degree (Phd students supervisor) Directeur: Rapporteur 1: Rapporteur 2: Membre du jury: Membre du jury: Membre du jury:}", | |
| } |
