David Delahaye
David Delahaye
Affiliation inconnue
Adresse e-mail validée de cnam.fr
Titre
Citée par
Citée par
Année
A tactic language for the system Coq
D Delahaye
International Conference on Logic for Programming Artificial Intelligence …, 2000
2532000
Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
R Bonichon, D Delahaye, D Doligez
International Conference on Logic for Programming Artificial Intelligence …, 2007
1462007
The Coq proof assistant reference manual
B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ...
INRIA, version 6 (11), 1999
961999
Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
D Delahaye, D Doligez, F Gilbert, P Halmagrand, O Hermant
International Conference on Logic for Programming Artificial Intelligence …, 2013
452013
Field: une procédure de décision pour les nombres réels en Coq
D Delahaye, M Mayero
JFLA: Journées Francophones des Langages Applicatifs, 1-16, 2001
402001
Dealing with algebraic expressions over a field in Coq using Maple
D Delahaye, M Mayero
Journal of Symbolic Computation 39 (5), 569-592, 2005
312005
Information retrieval in a Coq proof library using type isomorphisms
D Delahaye
International Workshop on Types for Proofs and Programs, 131-147, 1999
311999
Producing certified functional code from inductive specifications
PN Tollitte, D Delahaye, C Dubois
International Conference on Certified Programs and Proofs, 76-91, 2012
262012
A proof dedicated meta-language
D Delahaye
Electronic Notes in Theoretical Computer Science 70 (2), 96-109, 2002
262002
Certifying Airport Security Regulations Using the Focal Environment
D Delahaye, JF Étienne, VV Donzeau-Gouge
International Symposium on Formal Methods, 48-63, 2006
252006
The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations
D Delahaye, C Dubois, C Marché, D Mentré
International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and …, 2014
242014
Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving
M Jacquel, K Berkani, D Delahaye, C Dubois
International Conference on Software Engineering and Formal Methods, 253-268, 2011
212011
Dedukti: a logical framework based on the λΠ-calculus modulo theory
A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ...
Manuscript http://www. lsv. fr/~ dowek/Publi/expressing. pdf, 2016
202016
Automated deduction in the B set theory using typed proof search and deduction modulo
G Bury, D Delahaye, D Doligez, P Halmagrand, O Hermant
LPAR 20: 20th International Conference on Logic for Programming, Artificial …, 2015
202015
Dedukti: a logical framework based on the λ Π-calculus modulo theory, 2016
A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ...
URL: http://www. lsv. fr/~ dowek/Publi/expressing. pdf, 2019
172019
Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system
A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ...
22nd International Conference on Types for Proofs and Programs, 2016
152016
Producing UML models from focal specifications: an application to airport security regulations
D Delahaye, JF Etienne, VV Donzeau-Gouge
2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of …, 2008
152008
Recherche dans une bibliotheque de preuves Coq en utilisant filetype et modulo isomorphismes
D Delahaye, R Di Cosmo, B Werner
PRC/GDR de programmation, Pôle Preuves et Spécifications Algébriques, 1997
151997
Tableaux modulo theories using superdeduction
M Jacquel, K Berkani, D Delahaye, C Dubois
International Joint Conference on Automated Reasoning, 332-338, 2012
142012
Extracting purely functional contents from logical inductive types
D Delahaye, C Dubois, JF Étienne
International Conference on Theorem Proving in Higher Order Logics, 70-85, 2007
142007
Le système ne peut pas réaliser cette opération maintenant. Veuillez réessayer plus tard.
Articles 1–20