 | 2008 |
|---|
| 16 |       | David Delahaye,
Jean-Frédéric Étienne,
Véronique Donzeau-Gouge:
Producing UML Models from Focal Specifications: An Application to Airport Security Regulations.
TASE 2008: 121-124 |
| 15 | | David Delahaye,
Jean-Frédéric Étienne,
Véronique Donzeau-Gouge:
A formal and sound transformation from Focal to UML : an application to airport security regulations.
ISSE 4(3): 267-274 (2008) |
| 2007 |
|---|
| 14 | | Richard Bonichon,
David Delahaye,
Damien Doligez:
Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs.
LPAR 2007: 151-165 |
| 13 | | David Delahaye,
Catherine Dubois,
Jean-Frédéric Étienne:
Extracting Purely Functional Contents from Logical Inductive Types.
TPHOLs 2007: 70-85 |
| 2006 |
|---|
| 12 | | David Delahaye,
Jean-Frédéric Étienne,
Véronique Donzeau-Gouge:
Certifying Airport Security Regulations Using the Focal Environment.
FM 2006: 48-63 |
| 11 | | David Delahaye,
Jean-Frédéric Étienne,
Véronique Donzeau-Gouge:
Reasoning about Airport Security Regulations Using the Focal Environment.
ISoLA 2006: 45-52 |
| 10 | | David Delahaye,
Jean-Frédéric Étienne,
Véronique Donzeau-Gouge:
Modeling Airport Security Regulations in Focal.
ReMo2V 2006 |
| 9 | | 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 |
|---|
| 8 | | 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) |
| 7 | | David Delahaye,
Micaela Mayero:
Dealing with algebraic expressions over a field in Coq using Maple.
J. Symb. Comput. 39(5): 569-592 (2005) |
| 6 | | David Delahaye,
Mathieu Jaume,
Virgile Prevosto:
Coq, un outil pour l'enseignement. Une expérience avec les étudiants du DESS Développement de logiciels srs.
Technique et Science Informatiques 24(9): 1139-1160 (2005) |
| 2002 |
|---|
| 5 | | David Delahaye:
Free-Style Theorem Proving.
TPHOLs 2002: 164-181 |
| 4 | | 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 | | David Delahaye:
A Tactic Language for the System Coq.
LPAR 2000: 85-95 |
| 1999 |
|---|
| 1 | | David Delahaye:
Information Retrieval in a Coq Proof Library Using Type Isomorphisms.
TYPES 1999: 131-147 |
