Presentation of the research directorate
Proof assistants are particularly useful in the verification of hardware or software components for undecidable properties. In order to compensate for the lack of automaticity of the verification, these tools are interactive and accompanied by languages allowing to program demonstration strategies, or even to have automatic procedures on decidable fragments of the considered theory.
The Coq proof assistant is interesting for more than one reason:
- it is based on a very expressive language, the Calculation of Inductive Constructions containing intuitionistic higher order logic, and allowing the expression of programs and their specification, as well as the extraction of programs from the proof of feasibility of specifications;
- the reductions associated with this λ-calculus facilitate proof by reflection;
- the evidence is represented by λ-terms, the validity of statements obtained using the tactics is ensured by the type checker;
- evidence development tools do not need to be validated (De Bruijn criterion).
The activities on this research direction revolve around the following points:
- Formalization of the theory of local computations: proofs of distributed algorithms, proofs of properties of classes of algorithms (simulation, impossibility results) - Work in collaboration with the VISIDIA project;
- Study of the relations between Coq logic and mathematical language: Hilbert's choice operator, partial functions;
- Modelling and verification of safety properties of embedded systems, including specialised microprocessors such as smart cards.
The activities around this sub-theme therefore include practical aspects, particularly in the programming of methods of proof, and more fundamental aspects concerning the power of expression of various logical formalisms.