David Delahaye

37 papers A 2B 7C 5Misc 2Journal 9Unranked 10

Year	Rank	Type	Title / Venue / Authors
2023	J	`jnl`	Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory. CoRR Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard
2022	A	`conf`	Goéland: A Concurrent Tableau-Based Theorem Prover (System Description). IJCAR Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard, Hinde-Lilia Bouziane
2020	J	`jnl`	First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice. J. Autom. Reason. Guillaume Burel, Guillaume Bury, Raphaël Cauderlier, David Delahaye, Pierre Halmagrand, Olivier Hermant
2020	—	`conf`	Toward the Formal Verification of HILECOP: Formalization and Implementation of Synchronously Executed Petri Nets. PNSE@Petri Nets Vincent Iampietro, David Andreu, David Delahaye
2019	Misc	`conf`	Graph-Based Variability Modelling: Towards a Classification of Existing Formalisms. ICCS Jessie Carbonnel, David Delahaye, Marianne Huchard, Clémentine Nebut
2018	C	`conf`	An Automation-Friendly Set Theory for the B Method. ABZ Guillaume Bury, Simon Cruanes, David Delahaye, Pierre-Louis Euvrard
2018	—	`ed.`	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. SETS@ABZ Maximiliano Cristiá, David Delahaye, Catherine Dubois
2018	C	`conf`	Recovering Three-Level Architectures from the Code of Open-Source Java Spring Projects (S). SEKE Alexandre Le Borgne, David Delahaye, Marianne Huchard, Christelle Urtado, Sylvain Vauttier
2017	C	`conf`	Substitutability-Based Version Propagation to Manage the Evolution of Three-Level Component-Based Architectures. SEKE Alexandre Le Borgne, David Delahaye, Marianne Huchard, Christelle Urtado, Sylvain Vauttier
2015	—	`conf`	Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo. LPAR (short papers) Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, Olivier Hermant
2015	B	`conf`	Integrating Simplex with Tableaux. TABLEAUX Guillaume Bury, David Delahaye
2015	J	`jnl`	Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction. CoRR David Delahaye, Mélanie Jacquel
2015	J	`jnl`	Tableaux Modulo Theories Using Superdeduction. CoRR Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois
2015	J	`jnl`	Verifying B proof rules using deep embedding and automated theorem proving. Softw. Syst. Model. Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois
2014	C	`conf`	The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. ABZ David Delahaye, Catherine Dubois, Claude Marché, David Mentré
2013	B	`conf`	Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo. LPAR David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant
2012	B	`conf`	Producing Certified Functional Code from Inductive Specifications. CPP Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois
2012	A	`conf`	Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. IJCAR Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois
2011	B	`conf`	Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving. SEFM Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois
2010	—	`ed.`	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 AISC/MKM/Calculemus Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence Rideau, Renaud Rioboo, Alan P. Sexton
2008	J	`jnl`	A formal and sound transformation from Focal to UML : an application to airport security regulations. Innov. Syst. Softw. Eng. David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge
2008	—	`conf`	Formal Modeling of Airport Security Regulations using the Focal Environment. RELAW David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge
2008	Misc	`conf`	Producing UML Models from Focal Specifications: An Application to Airport Security Regulations. TASE David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge
2007	—	`conf`	Extracting Purely Functional Contents from Logical Inductive Types. TPHOLs David Delahaye, Catherine Dubois, Jean-Frédéric Étienne
2007	B	`conf`	Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. LPAR Richard Bonichon, David Delahaye, Damien Doligez
2006	B	`conf`	Certifying Airport Security Regulations Using the Focal Environment. FM David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge
2006	—	`conf`	Modeling Airport Security Regulations in Focal. ReMo2V David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge
2006	C	`conf`	Reasoning about Airport Security Regulations Using the Focal Environment. ISoLA David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge
2005	J	`jnl`	Coq, un outil pour l'enseignement. Une expérience avec les étudiants du DESS Développement de logiciels srs. Tech. Sci. Informatiques David Delahaye, Mathieu Jaume, Virgile Prevosto
2005	J	`jnl`	Dealing with algebraic expressions over a field in Coq using Maple. J. Symb. Comput. David Delahaye, Micaela Mayero
2005	J	`jnl`	Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant CoRR David Delahaye, Micaela Mayero
2005	—	`conf`	Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System. Calculemus David Delahaye, Micaela Mayero
2002	—	`conf`	A Proof Dedicated Meta-Language. LFM David Delahaye
2002	—	`conf`	Free-Style Theorem Proving. TPHOLs David Delahaye
2001	—	`conf`	Field, une procédure de décision pour les nombres réels en Coq. JFLA David Delahaye, Micaela Mayero
2000	B	`conf`	A Tactic Language for the System Coq. LPAR David Delahaye
1999	—	`conf`	Information Retrieval in a Coq Proof Library Using Type Isomorphisms. TYPES David Delahaye