Please note: This is a beta version of the new dblp website.
You can find the classic dblp view of this page here.
You can find the classic dblp view of this page here.
David Delahaye
2010 – today
- 2012
[c14]Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois: Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. IJCAR 2012: 332-338- [c13]Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois: Producing Certified Functional Code from Inductive Specifications. CPP 2012: 76-91
- 2011
- [c12]Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois: Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving. SEFM 2011: 253-268
- 2010
- [e1]Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence Rideau, Renaud Rioboo, Alan P. Sexton (Eds.): Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings. Lecture Notes in Computer Science 6167, Springer 2010, ISBN 978-3-642-14127-0
2000 – 2009
- 2008
- [j5]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)
- [c11]David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge: Formal Modeling of Airport Security Regulations using the Focal Environment. RELAW 2008: 16-20
- [c10]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
- 2007
- [c9]Richard Bonichon, David Delahaye, Damien Doligez: Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. LPAR 2007: 151-165
- [c8]David Delahaye, Catherine Dubois, Jean-Frédéric Étienne: Extracting Purely Functional Contents from Logical Inductive Types. TPHOLs 2007: 70-85
- 2006
- [j4]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)
- [c7]David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge: Modeling Airport Security Regulations in Focal. ReMo2V 2006
- [c6]David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge: Certifying Airport Security Regulations Using the Focal Environment. FM 2006: 48-63
- [c5]David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge: Reasoning about Airport Security Regulations Using the Focal Environment. ISoLA 2006: 45-52
- 2005
- [j3]David Delahaye, Micaela Mayero: Dealing with algebraic expressions over a field in Coq using Maple. J. Symb. Comput. 39(5): 569-592 (2005)
- [j2]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)
- [i1]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)
- 2002
- [j1]David Delahaye: A Proof Dedicated Meta-Language. Electr. Notes Theor. Comput. Sci. 70(2): 96-109 (2002)
- [c4]
- 2001
- [c3]David Delahaye, Micaela Mayero: Field, une procédure de décision pour les nombres réels en Coq. JFLA 2001: 33-48
- 2000
- [c2]
1990 – 1999
- 1999
- [c1]David Delahaye: Information Retrieval in a Coq Proof Library Using Type Isomorphisms. TYPES 1999: 131-147
Coauthor Index
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2012-12-02 20:31 CET by the dblp team