default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDDavid Delahaye
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2023
[i4]Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard:
Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory. CoRR abs/2311.07185 (2023)- 2022
- [c26]Julie Cailler
, Johann Rosain, David Delahaye, Simon Robillard, Hinde-Lilia Bouziane:
Goéland: A Concurrent Tableau-Based Theorem Prover (System Description). IJCAR 2022: 359-368 - 2020
- [j5]Guillaume Burel, Guillaume Bury, Raphaël Cauderlier, David Delahaye, Pierre Halmagrand, Olivier Hermant:
First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice. J. Autom. Reason. 64(6): 1001-1050 (2020) - [c25]Vincent Iampietro, David Andreu, David Delahaye:
Toward the Formal Verification of HILECOP: Formalization and Implementation of Synchronously Executed Petri Nets. PNSE@Petri Nets 2020: 214-215
2010 – 2019
- 2019
- [c24]Jessie Carbonnel, David Delahaye, Marianne Huchard, Clémentine Nebut:
Graph-Based Variability Modelling: Towards a Classification of Existing Formalisms. ICCS 2019: 27-41 - 2018
- [c23]Guillaume Bury, Simon Cruanes, David Delahaye, Pierre-Louis Euvrard:
An Automation-Friendly Set Theory for the B Method. ABZ 2018: 409-414 - [c22]Alexandre Le Borgne, David Delahaye, Marianne Huchard, Christelle Urtado, Sylvain Vauttier:
Recovering Three-Level Architectures from the Code of Open-Source Java Spring Projects (S). SEKE 2018: 199-198 - [e2]Maximiliano Cristiá, David Delahaye, Catherine Dubois:
Proceedings of the 3rd International Workshop on Sets and Tools co-located with the 6th International ABZ Conference, SETS@ABZ 2018, Southamptom, UK, June 5, 2018. CEUR Workshop Proceedings 2199, CEUR-WS.org 2018 [contents] - 2017
- [c21]Alexandre Le Borgne, David Delahaye, Marianne Huchard, Christelle Urtado, Sylvain Vauttier:
Substitutability-Based Version Propagation to Manage the Evolution of Three-Level Component-Based Architectures. SEKE 2017: 18-23 - 2015
- [j4]Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois:
Verifying B proof rules using deep embedding and automated theorem proving. Softw. Syst. Model. 14(1): 101-119 (2015) - [c20]Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, Olivier Hermant:
Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo. LPAR (short papers) 2015: 42-58 - [c19]Guillaume Bury, David Delahaye:
Integrating Simplex with Tableaux. TABLEAUX 2015: 86-101 - [i3]David Delahaye, Mélanie Jacquel:
Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction. CoRR abs/1501.01170 (2015) - [i2]Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois:
Tableaux Modulo Theories Using Superdeduction. CoRR abs/1501.01301 (2015) - 2014
- [c18]David Delahaye, Catherine Dubois, Claude Marché, David Mentré:
The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. ABZ 2014: 290-293 - 2013
- [c17]David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant:
Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo. LPAR 2013: 274-290 - 2012
- [c16]Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois:
Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. IJCAR 2012: 332-338 - [c15]Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois:
Producing Certified Functional Code from Inductive Specifications. CPP 2012: 76-91 - 2011
- [c14]Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois:
Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving. SEFM 2011: 253-268 - 2010
- [e1]Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence Rideau, Renaud Rioboo, Alan P. Sexton:
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. Lecture Notes in Computer Science 6167, Springer 2010, ISBN 978-3-642-14127-0 [contents]
2000 – 2009
- 2008
- [j3]David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge:
A formal and sound transformation from Focal to UML : an application to airport security regulations. Innov. Syst. Softw. Eng. 4(3): 267-274 (2008) - [c13]David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge:
Formal Modeling of Airport Security Regulations using the Focal Environment. RELAW 2008: 16-20 - [c12]David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge:
Producing UML Models from Focal Specifications: An Application to Airport Security Regulations. TASE 2008: 121-124 - 2007
- [c11]Richard Bonichon, David Delahaye, Damien Doligez:
Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. LPAR 2007: 151-165 - [c10]David Delahaye, Catherine Dubois, Jean-Frédéric Étienne:
Extracting Purely Functional Contents from Logical Inductive Types. TPHOLs 2007: 70-85 - 2006
- [c9]David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge:
Modeling Airport Security Regulations in Focal. ReMo2V 2006 - [c8]David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge:
Certifying Airport Security Regulations Using the Focal Environment. FM 2006: 48-63 - [c7]David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge:
Reasoning about Airport Security Regulations Using the Focal Environment. ISoLA 2006: 45-52 - 2005
- [j2]David Delahaye, Micaela Mayero:
Dealing with algebraic expressions over a field in Coq using Maple. J. Symb. Comput. 39(5): 569-592 (2005) - [j1]David Delahaye, Mathieu Jaume, Virgile Prevosto:
Coq, un outil pour l'enseignement. Une expérience avec les étudiants du DESS Développement de logiciels srs. Tech. Sci. Informatiques 24(9): 1139-1160 (2005) - [c6]David Delahaye, Micaela Mayero:
Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System. Calculemus 2005: 57-73 - [i1]David Delahaye, Micaela Mayero:
Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant. CoRR abs/cs/0510011 (2005) - 2002
- [c5]David Delahaye:
Free-Style Theorem Proving. TPHOLs 2002: 164-181 - [c4]David Delahaye:
A Proof Dedicated Meta-Language. LFM 2002: 96-109 - 2001
- [c3]David Delahaye, Micaela Mayero:
Field, une procédure de décision pour les nombres réels en Coq. JFLA 2001: 33-48 - 2000
- [c2]David Delahaye:
A Tactic Language for the System Coq. LPAR 2000: 85-95
1990 – 1999
- 1999
- [c1]David Delahaye:
Information Retrieval in a Coq Proof Library Using Type Isomorphisms. TYPES 1999: 131-147
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 21:25 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
