Information Retrieval in a Coq Proof Library Using Type Isomorphisms. - David Delahaye (TYPES, 1999)

A Tactic Language for the System Coq. - David Delahaye (LPAR, 2000)

Field, une procédure de décision pour les nombres réels en Coq. - David Delahaye; Micaela Mayero (JFLA, 2001)

Free-Style Theorem Proving. - David Delahaye (TPHOLs, 2002)

A Proof Dedicated Meta-Language. - David Delahaye (LFM, 2002)

Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant - David Delahaye; Micaela Mayero (CoRR, 2005)

Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System. - David Delahaye; Micaela Mayero (Calculemus, 2005)

Dealing with algebraic expressions over a field in Coq using Maple. - David Delahaye; Micaela Mayero (J. Symb. Comput., 2005)

Coq, un outil pour l'enseignement. Une expérience avec les étudiants du DESS Développement de logiciels srs. - David Delahaye; Mathieu Jaume; Virgile Prevosto (Tech. Sci. Informatiques, 2005)

Modeling Airport Security Regulations in Focal. - David Delahaye; Jean-Frédéric Étienne; Véronique Donzeau-Gouge (ReMo2V, 2006)

Certifying Airport Security Regulations Using the Focal Environment. - David Delahaye; Jean-Frédéric Étienne; Véronique Donzeau-Gouge (FM, 2006)

Reasoning about Airport Security Regulations Using the Focal Environment. - David Delahaye; Jean-Frédéric Étienne; Véronique Donzeau-Gouge (ISoLA, 2006)

Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. - Richard Bonichon; David Delahaye; Damien Doligez (LPAR, 2007)

Extracting Purely Functional Contents from Logical Inductive Types. - David Delahaye; Catherine Dubois; Jean-Frédéric Étienne (TPHOLs, 2007)

Formal Modeling of Airport Security Regulations using the Focal Environment. - David Delahaye; Jean-Frédéric Étienne; Véronique Donzeau-Gouge (RELAW, 2008)

Producing UML Models from Focal Specifications: An Application to Airport Security Regulations. - David Delahaye; Jean-Frédéric Étienne; Véronique Donzeau-Gouge (TASE, 2008)

A formal and sound transformation from Focal to UML : an application to airport security regulations. - David Delahaye; Jean-Frédéric Étienne; Véronique Donzeau-Gouge (Innov. Syst. Softw. Eng., 2008)

Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. - Mélanie Jacquel; Karim Berkani; David Delahaye; Catherine Dubois (IJCAR, 2012)

Producing Certified Functional Code from Inductive Specifications. - Pierre-Nicolas Tollitte; David Delahaye; Catherine Dubois (CPP, 2012)

Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo. - David Delahaye; Damien Doligez; Frédéric Gilbert 002; Pierre Halmagrand; Olivier Hermant (LPAR, 2013)

The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. - David Delahaye; Catherine Dubois; Claude Marché; David Mentré (ABZ, 2014)

Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo. - Guillaume Bury; David Delahaye; Damien Doligez; Pierre Halmagrand; Olivier Hermant (LPAR (short papers), 2015)

Integrating Simplex with Tableaux. - Guillaume Bury; David Delahaye (TABLEAUX, 2015)

Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction. - David Delahaye; Mélanie Jacquel (CoRR, 2015)

Tableaux Modulo Theories Using Superdeduction. - Mélanie Jacquel; Karim Berkani; David Delahaye; Catherine Dubois (CoRR, 2015)

Verifying B proof rules using deep embedding and automated theorem proving. - Mélanie Jacquel; Karim Berkani; David Delahaye; Catherine Dubois (Softw. Syst. Model., 2015)

Substitutability-Based Version Propagation to Manage the Evolution of Three-Level Component-Based Architectures. - Alexandre Le Borgne; David Delahaye; Marianne Huchard; Christelle Urtado; Sylvain Vauttier (SEKE, 2017)

An Automation-Friendly Set Theory for the B Method. - Guillaume Bury; Simon Cruanes; David Delahaye; Pierre-Louis Euvrard (ABZ, 2018)

Recovering Three-Level Architectures from the Code of Open-Source Java Spring Projects (S). - Alexandre Le Borgne; David Delahaye; Marianne Huchard; Christelle Urtado; Sylvain Vauttier (SEKE, 2018)

Graph-Based Variability Modelling: Towards a Classification of Existing Formalisms. - Jessie Carbonnel; David Delahaye; Marianne Huchard; Clémentine Nebut (ICCS, 2019)

Toward the Formal Verification of HILECOP: Formalization and Implementation of Synchronously Executed Petri Nets. - Vincent Iampietro; David Andreu 001; David Delahaye (PNSE@Petri Nets, 2020)

First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice. - Guillaume Burel; Guillaume Bury; Raphaël Cauderlier; David Delahaye; Pierre Halmagrand; Olivier Hermant (J. Autom. Reason., 2020)

Goéland: A Concurrent Tableau-Based Theorem Prover (System Description). - Julie Cailler; Johann Rosain; David Delahaye; Simon Robillard; Hinde-Lilia Bouziane (IJCAR, 2022)

Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory. - Ali Assaf 002; Guillaume Burel; Raphaël Cauderlier; David Delahaye; Gilles Dowek; Catherine Dubois; Frédéric Gilbert 002; Pierre Halmagrand; Olivier Hermant; Ronan Saillard (CoRR, 2023)