| 2007 |
|---|
| 11 | EE | Richard Bonichon,
David Delahaye,
Damien Doligez:
Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs.
LPAR 2007: 151-165 |
| 10 | EE | David Delahaye,
Catherine Dubois,
Jean-Frédéric Étienne:
Extracting Purely Functional Contents from Logical Inductive Types.
TPHOLs 2007: 70-85 |
| 2006 |
|---|
| 9 | EE | David Delahaye,
Jean-Frédéric Étienne,
Véronique Donzeau-Gouge:
Certifying Airport Security Regulations Using the Focal Environment.
FM 2006: 48-63 |
| 8 | EE | David Delahaye,
Micaela Mayero:
Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System.
Electr. Notes Theor. Comput. Sci. 151(1): 57-73 (2006) |
| 2005 |
|---|
| 7 | EE | David Delahaye,
Micaela Mayero:
Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant
CoRR abs/cs/0510011: (2005) |
| 6 | EE | David Delahaye,
Micaela Mayero:
Dealing with algebraic expressions over a field in Coq using Maple.
J. Symb. Comput. 39(5): 569-592 (2005) |
| 2002 |
|---|
| 5 | EE | David Delahaye:
Free-Style Theorem Proving.
TPHOLs 2002: 164-181 |
| 4 | EE | David Delahaye:
A Proof Dedicated Meta-Language.
Electr. Notes Theor. Comput. Sci. 70(2): (2002) |
| 2001 |
|---|
| 3 | | David Delahaye,
Micaela Mayero:
Field, une procédure de décision pour les nombres réels en Coq.
JFLA 2001: 33-48 |
| 2000 |
|---|
| 2 | EE | David Delahaye:
A Tactic Language for the System Coq.
LPAR 2000: 85-95 |
| 1999 |
|---|
| 1 | EE | David Delahaye:
Information Retrieval in a Coq Proof Library Using Type Isomorphisms.
TYPES 1999: 131-147 |
