| A tactic language for the system Coq D Delahaye LPAR 1955, 85-95, 2000 | 282 | 2000 |
| Zenon: An extensible automated theorem prover producing checkable proofs R Bonichon, D Delahaye, D Doligez LPAR 4790, 151-165, 2007 | 155 | 2007 |
| The Coq proof assistant reference manual B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ... INRIA, version 6 (11), 1999 | 115 | 1999 |
| Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo D Delahaye, D Doligez, F Gilbert, P Halmagrand, O Hermant Logic for Programming, Artificial Intelligence, and Reasoning: 19th …, 2013 | 47 | 2013 |
| 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 | 41 | 2001 |
| Dealing with algebraic expressions over a field in Coq using Maple D Delahaye, M Mayero Journal of Symbolic Computation 39 (5), 569-592, 2005 | 32 | 2005 |
| Information retrieval in a Coq proof library using type isomorphisms D Delahaye Types for Proofs and Programs: International Workshop, TYPES’99 Lökeberg …, 2000 | 32 | 2000 |
| Producing certified functional code from inductive specifications PN Tollitte, D Delahaye, C Dubois Certified Programs and Proofs: Second International Conference, CPP 2012 …, 2012 | 28 | 2012 |
| A proof dedicated meta-language D Delahaye Electronic Notes in Theoretical Computer Science 70 (2), 96-109, 2002 | 27 | 2002 |
| The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations D Delahaye, C Dubois, C Marché, D Mentré Abstract State Machines, Alloy, B, TLA, VDM, and Z: 4th International …, 2014 | 25 | 2014 |
| Certifying Airport Security Regulations Using the Focal Environment D Delahaye, JF Étienne, VV Donzeau-Gouge FM 2006: Formal Methods: 14th International Symposium on Formal Methods …, 2006 | 25 | 2006 |
| 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 | 24 | 2016 |
| 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 | 21 | 2015 |
| 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, ... TYPES: Types for Proofs and Programs, 2016 | 20 | 2016 |
| Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving. M Jacquel, K Berkani, D Delahaye, C Dubois SEFM 7041, 253-268, 2011 | 20 | 2011 |
| Dedukti: a logical framework based on the λ Π-calculus modulo theory, 2019 A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ... URL: http://www. lsv. fr/~ dowek/Publi/expressing. pdf, 2019 | 18 | 2019 |
| 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 | 17 | 1997 |
| 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 | 16 | 2008 |
| Conception de Langages pour Décrire les Preuves et les Automatisations dans les Outils d’Aidea la Preuve D Delahaye Thèese de doctorat, Universit e Paris 6, 2001 | 16 | 2001 |
| Extracting purely functional contents from logical inductive types D Delahaye, C Dubois, JF Étienne Theorem Proving in Higher Order Logics: 20th International Conference …, 2007 | 15 | 2007 |
