Folgen
David Delahaye
David Delahaye
Zugehörigkeit unbekannt
Bestätigte E-Mail-Adresse bei cnam.fr
Titel
Zitiert von
Zitiert von
Jahr
A tactic language for the system Coq
D Delahaye
Logic for Programming and Automated Reasoning: 7th International Conference …, 2000
3012000
Zenon: An extensible automated theorem prover producing checkable proofs
R Bonichon, D Delahaye, D Doligez
International Conference on Logic for Programming Artificial Intelligence …, 2007
1612007
The Coq proof assistant reference manual
B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ...
INRIA, version 6 (11), 1999
1301999
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
482013
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
432001
Information retrieval in a Coq proof library using type isomorphisms
D Delahaye
International Workshop on Types for Proofs and Programs, 131-147, 1999
331999
Dedukti: a logical framework based on the λΠ-calculus modulo theory
A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ...
322016
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
Producing certified functional code from inductive specifications
PN Tollitte, D Delahaye, C Dubois
International Conference on Certified Programs and Proofs, 76-91, 2012
292012
A proof dedicated meta-language
D Delahaye
Electronic Notes in Theoretical Computer Science 70 (2), 96-109, 2002
292002
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
262016
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
262014
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
252019
Certifying airport security regulations using the Focal environment
D Delahaye, JF Étienne, VV Donzeau-Gouge
International Symposium on Formal Methods, 48-63, 2006
252006
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
242015
Intelligent computer mathematics
S Autexier, J Calmet, D Delahaye, PDF Ion, L Rideau, R Rioboo, ...
Lecture Notes in Computer Science 6167, 2010
242010
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
202011
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
172001
Tableaux modulo theories using superdeduction: An application to the verification of B proof rules with the Zenon automated theorem prover
M Jacquel, K Berkani, D Delahaye, C Dubois
International Joint Conference on Automated Reasoning, 332-338, 2012
152012
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
Das System kann den Vorgang jetzt nicht ausführen. Versuchen Sie es später erneut.
Artikel 1–20