David Delahaye

Emails:

David.Delahaye@lirmm.fr
David.Delahaye@umontpellier.fr

Tel.:
Fax:

(+33) (0)4 67 41 86 01
(+33) (0)4 67 41 85 00

Address:

        Université de Montpellier
        LIRMM UMR 5506, CC477
        161 rue Ada
        34095 Montpellier Cedex 5
        France

To come:

see this page

Location:

Building 4 Ext Floor 2
Room E3.12

ResearchGate profile:

here

LinkedIn profile:

here

Viadeo profile:

here

Research

Zenon Automated Theorem Prover: I have contributed to the development of Zenon (used, inter alia, by the Focalize environment). In particular, I have realized the first version of the translation of Zenon proofs into proofs that can be checked by Coq.

Superdeduction: I have realized an extension of Zenon to superdeduction, called Super Zenon, which allows us to reason modulo a theory by integrating this theory with "compiled" deduction rules. I have also developed an instantiation of this extension to the B set theory.
Verification of B Proof Rules: in the framework of Atelier B and in collaboration with Siemens, I have applied Zenon to the verification of proof rules. In particular, I have used the extension of Zenon to superdeduction instantiated to the B set theory.

Inductive Relations: This consists in extracting a function from an inductive relation, in particular in the framework of the Calculus of Inductive Constructions. An implementation has been realized for the Coq proof assistant, as well as for the Focalize environment.
Proof Languages: It was the topic of my PhD thesis with the design of two kinds of languages for the Coq proof assistant. The first one is a language that allows us to describe proofs using several proof styles. The secod one is a language that allows us to describe proof automation directly within the proof assistant (called Ltac).
Type Isomorphisms: It was the topic of my Master thesis with the design of an information retrieval tool in a Coq proof library using type isomorphisms. To do so, the existing theory for ML has been adapted to deal with the dependent types of Coq.

Compiler: I contribute to the development of the Focalize compiler, in particular to the translations to OCaml and Coq. I have also proposed a module-based compilation scheme, which allows us to ensure a greater traceability w.r.t. the initial Focalize specifications.
Modeling: in the framework of the EDEMOI project, I have applied the Focalize environment to a concrete case-study, i.e. the regulations regarding airport security. Several formal models have been realized, including the international and European regulations in particular.
Documentation: still in the framework of the EDEMOI project, I have realized an extension of the compiler that allows us to produce UML models from Focalize specifications. This extension allows us to provide documentation for Focalize specifications, not only for developers, but also for users (such as certification authorities, for example).

Maple Mode for Coq: I have realized an interface between Coq and Maple in order to import into Coq computations over fields performed by Maple. The approach is "skeptical", i.e. all the imported computations are systematically (and automatically) certified.
Algebraically Closed Fields: I have developed a proof procedure for Coq that allows us to solve systems of polynomial equations and inequations over algebraically closed fields. This procedure extends the Maple mode for Coq by importing gcd computations from Maple in particular.
Real Closed Fields: I have implemented a test procedure for Focalize that allows us to verify the validity of first order properties over real closed fields by using a cylindrical algebraic decomposition performed by an Axiom routine. This procedure allows us to increase the confidence in the consistency of a given Focalize specification.