| A tactic language for the system Coq D Delahaye Logic for Programming and Automated Reasoning: 7th International Conference …, 2000 | 316 | 2000 |
| Zenon: An extensible automated theorem prover producing checkable proofs R Bonichon, D Delahaye, D Doligez International Conference on Logic for Programming Artificial Intelligence …, 2007 | 164 | 2007 |
| The Coq proof assistant reference manual B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ... INRIA, version 6 (11), 17-21, 1999 | 137 | 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 | 51 | 2013 |
| Dedukti: a logical framework based on the λΠ-calculus modulo theory A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ... | 41 | 2016 |
| 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 | 40 | 2001 |
| Information retrieval in a Coq proof library using type isomorphisms D Delahaye International Workshop on Types for Proofs and Programs, 131-147, 1999 | 34 | 1999 |
| 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 | 33 | 2016 |
| A proof dedicated meta-language D Delahaye Electronic Notes in Theoretical Computer Science 70 (2), 96-109, 2002 | 32 | 2002 |
| 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 | 31 | 2014 |
| Producing certified functional code from inductive specifications PN Tollitte, D Delahaye, C Dubois International Conference on Certified Programs and Proofs, 76-91, 2012 | 30 | 2012 |
| Dealing with algebraic expressions over a field in Coq using Maple D Delahaye, M Mayero Journal of Symbolic Computation 39 (5), 569-592, 2005 | 30 | 2005 |
| 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 | 26 | 2019 |
| 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 | 25 | 2015 |
| Intelligent computer mathematics S Autexier, J Calmet, D Delahaye, PDF Ion, L Rideau, R Rioboo, ... Lecture Notes in Computer Science 6167, 2010 | 25 | 2010 |
| Certifying airport security regulations using the Focal environment D Delahaye, JF Étienne, VV Donzeau-Gouge International Symposium on Formal Methods, 48-63, 2006 | 24 | 2006 |
| 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 | 20 | 2011 |
| 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 |
| 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 | 15 | 2008 |
| 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 | 15 | 2007 |
