×

zbMATH — the first resource for mathematics

Delahaye, David

Compute Distance To:
Author ID: delahaye.david Recent zbMATH articles by "Delahaye, David"
Published as: Delahaye; Delahaye, David
Documents Indexed: 17 Publications since 1946, including 2 Books

Publications by Year

Citations contained in zbMATH Open

13 Publications have been cited 52 times in 42 Documents Cited by Year
Zenon: An extensible automated theorem prover producing checkable proofs. Zbl 1137.68572
Bonichon, Richard; Delahaye, David; Doligez, Damien
12
2007
A tactic language for the system Coq. Zbl 0988.68584
Delahaye, David
11
2000
Zenon modulo: when Achilles outruns the tortoise using deduction modulo. Zbl 1406.68105
Delahaye, David; Doligez, Damien; Gilbert, Frédéric; Halmagrand, Pierre; Hermant, Olivier
6
2013
Dealing with algebraic expressions over a field in Coq using Maple. Zbl 1126.68101
Delahaye, David; Mayero, Micaela
5
2005
Information retrieval in a Coq proof library using type isomorphisms. Zbl 0988.68542
Delahaye, David
4
2000
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. Zbl 1194.68011
Autexier, Serge (ed.); Calmet, Jacques (ed.); Delahaye, David (ed.); Ion, Patrick D. F. (ed.); Rideau, Laurence (ed.); Rioboo, Renaud (ed.); Sexton, Alan P. (ed.)
3
2010
Extracting purely functional contents from logical inductive types. Zbl 1144.68354
Delahaye, David; Dubois, Catherine; Étienne, Jean-Frédéric
3
2007
Verifying B proof rules using deep embedding and automated theorem proving. Zbl 1350.68236
Jacquel, Mélanie; Berkani, Karim; Delahaye, David; Dubois, Catherine
2
2011
A proof dedicated meta-language. Zbl 1270.68262
Delahaye, David
2
2002
All about proofs, proofs for all. Zbl 1334.03007
Woltzenlogel Paleo, Bruno (ed.); Delahaye, David (ed.)
1
2015
Integrating simplex with tableaux. Zbl 06519936
Bury, Guillaume; Delahaye, David
1
2015
Tableaux modulo theories using superdeduction. An application to the verification of B proof rules with the Zenon automated theorem prover. Zbl 1358.68255
Jacquel, Mélanie; Berkani, Karim; Delahaye, David; Dubois, Catherine
1
2012
Quantifier elimination over algebraically closed fields in a proof assistant using a computer algebra system. Zbl 1273.68417
Delahaye, David; Mayero, Micaela
1
2006
All about proofs, proofs for all. Zbl 1334.03007
Woltzenlogel Paleo, Bruno (ed.); Delahaye, David (ed.)
1
2015
Integrating simplex with tableaux. Zbl 06519936
Bury, Guillaume; Delahaye, David
1
2015
Zenon modulo: when Achilles outruns the tortoise using deduction modulo. Zbl 1406.68105
Delahaye, David; Doligez, Damien; Gilbert, Frédéric; Halmagrand, Pierre; Hermant, Olivier
6
2013
Tableaux modulo theories using superdeduction. An application to the verification of B proof rules with the Zenon automated theorem prover. Zbl 1358.68255
Jacquel, Mélanie; Berkani, Karim; Delahaye, David; Dubois, Catherine
1
2012
Verifying B proof rules using deep embedding and automated theorem proving. Zbl 1350.68236
Jacquel, Mélanie; Berkani, Karim; Delahaye, David; Dubois, Catherine
2
2011
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. Zbl 1194.68011
Autexier, Serge (ed.); Calmet, Jacques (ed.); Delahaye, David (ed.); Ion, Patrick D. F. (ed.); Rideau, Laurence (ed.); Rioboo, Renaud (ed.); Sexton, Alan P. (ed.)
3
2010
Zenon: An extensible automated theorem prover producing checkable proofs. Zbl 1137.68572
Bonichon, Richard; Delahaye, David; Doligez, Damien
12
2007
Extracting purely functional contents from logical inductive types. Zbl 1144.68354
Delahaye, David; Dubois, Catherine; Étienne, Jean-Frédéric
3
2007
Quantifier elimination over algebraically closed fields in a proof assistant using a computer algebra system. Zbl 1273.68417
Delahaye, David; Mayero, Micaela
1
2006
Dealing with algebraic expressions over a field in Coq using Maple. Zbl 1126.68101
Delahaye, David; Mayero, Micaela
5
2005
A proof dedicated meta-language. Zbl 1270.68262
Delahaye, David
2
2002
A tactic language for the system Coq. Zbl 0988.68584
Delahaye, David
11
2000
Information retrieval in a Coq proof library using type isomorphisms. Zbl 0988.68542
Delahaye, David
4
2000
all top 5

Cited by 79 Authors

4 Sacerdoti Coen, Claudio
4 Urban, Josef
3 Delahaye, David
3 Kaliszyk, Cezary
2 Bury, Guillaume
2 Cauderlier, Raphaël
2 Dubois, Catherine
2 Gauthier, Thibault
2 Guidi, Ferruccio
2 Halmagrand, Pierre
2 Hermant, Olivier
2 Kohlhase, Michael
2 Komendantsky, Vladimir
2 Konovalov, Alexander B.
2 Leroy, Xavier
2 Linton, Steve A.
2 Rabe, Florian
1 Alama, Jesse
1 Appel, Andrew W.
1 Asperti, Andrea
1 Aspinall, David
1 Barthe, Gilles
1 Berghofer, Stefan
1 Berkani, Karim
1 Bertot, Yves
1 Bezem, Marc
1 Blazy, Sandrine
1 Brady, Edwin C.
1 Brink, Kasper
1 Bulwahn, Lukas
1 Burel, Guillaume
1 Cairns, Paul
1 Choppy, Christine
1 Conchon, Sylvain
1 Courtieu, Pierre
1 Cristiá, Maximiliano
1 Demange, Vincent
1 Denney, Ewen
1 Dietrich, Dominik
1 Dockins, Robert
1 Dos Reis, Gabriel
1 Dufay, Guillaume
1 Gilbert, Frédéric
1 Gow, Jeremy
1 Haftmann, Florian
1 Hendriks, Dimitri
1 Iancu, Mihnea
1 Jacquel, Mélanie
1 Ji, Kailiang
1 Kirchner, Florent
1 Kirchner, Hélène
1 Kumar, Ramana
1 Lescuyer, Stéphane
1 Li, Yue
1 Lüth, Christoph
1 Mahboubi, Assia
1 Malecha, Gregory
1 Mamane, Lionel Elie
1 Matichuk, Daniel
1 Matthews, David E.
1 Mayero, Micaela
1 Melo de Sousa, Simão
1 Morrisett, Greg
1 Muñoz, César A.
1 Murray, Toby
1 Norrish, Michael
1 Petrucci, Laure
1 Ricciotti, Wilmer
1 Rioboo, Renaud
1 Rossi, Gianfranco
1 Schulz, Ewaryst
1 Sibut-Pinote, Thomas
1 Slama, Franck
1 Stratulat, Sorin
1 Sutcliffe, Geoff
1 Tassi, Enrico
1 Wenzel, Makarius
1 Wisnesky, Ryan
1 Woltzenlogel Paleo, Bruno

Citations by Year