Nombre de documents

40

David Delahaye


Article dans une revue9 documents

  • Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois. Tableaux Modulo Theories Using Superdeduction. Global Journal of Advanced Software Engineering (GJASE), Avanti Publishers, 2014, 1, pp.1 - 13. <http://www.avantipublishers.com/downloads/gjasev1n1a1/>. <10.1007/978-3-642-31365-3_26>. <hal-01099338>
  • David Delahaye, Mélanie Jacquel. Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction. electronic Journal of Mathematics and Technology, 2013, 7 (2), pp.1 - 20. <https://php.radford.edu/~ejmt/ContentIndex.php#v7n2>. <hal-01099371>
  • Karim Berkani, David Delahaye, Catherine Dubois, Mélanie Jacquel, Martin Keogh, et al.. BCARe : un environnement pour la vérification de règles de l'Atelier B. Approches Formelles dans l'Assistance au Développement de Logiciels, 2012, pp.46-49. <hal-00722385>
  • Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois. Tableaux Modulo Theories using Superdeduction - An Application to the Veri fication of B Proof Rules with the Zenon Automated Theorem Prover. Journal of Automated Reasoning, Springer Verlag, 2012, 7364, pp.332-338. <10.1007/978-3-642-31365-3_26>. <hal-00722376>
  • Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois. Verifying B Proof Rules using Deep Embedding and Automated Theorem Proving. Software Engineering and Formal Methods, 2011, 7041, pp.253-268. <10.1007/978-3-642-24690-6_18>. <hal-00722373>
  • David Delahaye, Micaela Mayero. Dealing with Algebraic Expressions over a Field in Coq using Maple. J. Sc. Comp. (JSC), Springer, 2005, 39, pp.569-592. <hal-01125074>
  • David Delahaye, Mathieu Jaume, Virgile Prévosto. Coq : un outil pour l'enseignement. Technique et Science Informatiques, Editions Hermes, 2005, 24 (9), pp.1139-1160. <10.3166/tsi.24.1139-1160>. <hal-01195849>
  • David Delahaye, Mathieu Jaume, Virgile Prévosto. Coq: un outil pour l'enseignement. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2005, 24, pp.1139-1160. <hal-01125076>
  • E. Hauchard, David Delahaye, Pierre Frankhauser. Analyse morphologique de talwegs et comportement scalant : applications des dimensions non-entières à la géographie physique. Espace Geographique, Éditions Belin, 1999, 28 (3), pp.215-224. <halshs-00873169>

Communication dans un congrès27 documents

  • 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 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. <hal-01204701v2>
  • Guillaume Bury, David Delahaye. Integrating Simplex with Tableaux. Hans de Nivelle. Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2015, Wrowlaw, Poland. Lecture notes in computer science, pp.86-101, 2015, 24th International Conference, TABLEAUX 2015, Wrocław, Poland, September 21–24, 2015. Proceedings. <10.1007/978-3-319-24312-2_7>. <hal-01215490>
  • David Delahaye, Catherine Dubois, Claude Marché, David Mentré. The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. Abstract State Machines, Alloy, B, VDM, and Z, Jun 2014, Toulouse, France. Springer, 8477, pp.290-293, 2014, Lecture Notes in Computer Science. <hal-00998092>
  • David Delahaye, Claude Marché, David Mentré. Le projet BWare : une plate-forme pour la vérification automatique d'obligations de preuve B. Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2014, Paris, France. EasyChair, 2014. <hal-00998094>
  • David Delahaye. Automated Deduction Modulo. Proof-Search in Axiomatic Theories and Type Theories (PSATTT), Nov 2013, Palaiseau, France. 2013. <hal-01126339>
  • David Delahaye, Catherine Dubois, Pierre-Nicolas Tollitte. RelExt : Synthèse de code à partir de spécifications inductives. AFADL 2013, Apr 2013, Nancy, France. 4 p., 2013. <hal-01126320>
  • David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant. Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo. Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. Springer, 8312, pp.274-290, 2013, LNCS; Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings. <10.1007/978-3-642-45221-5_20>. <hal-00909784>
  • David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant. Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps. Stephan Schulz and Geoff Sutcliffe and Boris Konev. IWIL - 10th International Workshop on the Implementation of Logics - 2013, Dec 2013, Stellenbosch, South Africa. EasyChair, 2013. <hal-00909688>
  • 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. International Joint Conference on Automated Reasoning (IJCAR 2012), Jun 2012, Manchester, Ukraine. 7364, pp.332--338, 2012, LNAI. <hal-01126134>
  • Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois. Producing Certified Functional Code from Inductive Specifications. International Conference on Certified Programs and Proofs (CPP 2012), Dec 2012, Kyoto, Japan. 7679, pp.76-91, 2012, LNCS. <hal-01126212>
  • Karim Berkani, David Delahaye, Catherine Dubois, Mélanie Jacquel, Martin Keogh, et al.. BCARe : un environnement pour la vérification de règles de l?Atelier B. Approches Formelles dans l'Assistance au D?veloppement de Logiciels (AFADL 2012), Jan 2012, Grenoble, France. pp.46-49, 2012. <hal-01126033>
  • David Delahaye, Catherine Dubois, Pierre-Nicolas Tollitte. Génération de code fonctionnel certifié à partir de spécifications inductives dans l'environnement Focalize. Journ?es Francophones des Langages Applicatifs (JFLA'10), Jan 2010, La Ciotat, France. pp.55-81, 2010, Studia informatica universalis. <hal-01125723>
  • David Delahaye, Jean-Frédéric Etienne, Veronique Viguie Donzeau-Gouge. Producing UML Models from Focal Specifications: An Application to Airport Security Regulations. TASE'08 Theoretical Aspects of Software Engineering, Nanjing (China), Jan 2008, X, France. pp.121-124, 2008. <hal-01125582>
  • David Delahaye, Jean-Frédéric Etienne, Veronique Viguie Donzeau-Gouge. Formal Modeling of Airport Security Regulations using the Focal Environment. RELAW'08 Requirements Engineering and Law, Barcelona (Spain), Jan 2008, X, France. pp.16-20, 2008. <hal-01125583>
  • David Delahaye, Jean-Frédéric Etienne, Veronique Viguie Donzeau-Gouge. A Formal and Sound Transformation from Focal to UML: An Application to Airport Security Regulations. UMLFM'08 UML and Formal Methods, Kitakyushu-City (Japan), Jan 2008, X, France. 4, pp.267-274, 2008, ISSE. <hal-01125584>
  • Philippe Ayrault, Matthieu Carlier, David Delahaye, Catherine Dubois, Damien Doligez, et al.. Trusted Software within Focal. C&ESAR 2008 - Computer & Electronics Security Applications Rendez-vous, Dec 2008, Rennes, France. Trusting Trusted Computing ?, pp.162-179, 2008. <hal-01125667v2>
  • David Delahaye, Catherine Dubois, Jean-Frédéric Etienne. Extracting Purely Functional Contents from Logical Inductive Types. TPHOLs'07 Theorem Proving in Higher Order Logics, Kaiserslautern (Germany), Jan 2007, X, France. 4732, pp.70-85, 2007, LNCS. <hal-01125370>
  • Richard Bonichon, David Delahaye, Damien Doligez. Zenon: an Extensible Automated Theorem Prover Producing Checkable Proofs. Logic for Programming, Artificial Intelligence, and Reasoning, Oct 2007, Yerevan, Armenia. Springer, 4790, pp.151-165, 2007, Lecture Notes in Computer Science; Logic for Programming, Artificial Intelligence, and Reasoning. <10.1007/978-3-540-75560-9_13>. <inria-00315920>
  • David Delahaye, Jean-Frédéric Etienne, Veronique Viguie Donzeau-Gouge. Reasoning about Airport Security Regulations using the Focal Environment. ISoLA, Paphos (Cyprus), Jan 2006, X, France. pp.36-44, 2006. <hal-01125369>
  • David Delahaye, Jean-Frédéric Etienne, Veronique Viguie Donzeau-Gouge. Modeling Airport Security Regulations in Focal. REMO2V'06 Regulations Modelling and their Validation Verification, Luxembourg, Jan 2006, X, France. pp.806-812, 2006. <hal-01125367>
  • David Delahaye, Jean-Frédéric Etienne, Veronique Viguie Donzeau-Gouge. Certifying Airport Security Regulations using the Focal Environment. FM'06: 14th Symposium on Formal Methods, Hamilton, Canada, Jan 2006, X, France. 4085, pp.48-63, 2006, LNCS. <hal-01125368>
  • David Delahaye, Micaela Mayero. Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System. Calculemus, University of Newcastle upon Tyn (United Kingdom), Jan 2005, X, France. 151, pp.57-73, 2005, ENTCS. <hal-01125075>
  • David Delahaye. A Proof Dedicated Meta-Language. Proceedings of Logical Frameworks and Meta-Languages (LFM), Copenhagen (Denmark), Jan 2002, X, France. 70, 2002, ENTCS. <hal-01125072>
  • David Delahaye. Free-style Theorem Proving. Proceedings of Theorem Proving in Higher Order Logics (TPHOLs), Hampton (VA, USA), Jan 2002, X, France. 2410, pp.164-181, 2002, LNCS. <hal-01125073>
  • David Delahaye, Micaela Mayero. Field: une procédure de décision pour les nombres réels en Coq. Journées Francophones des Langages Applicatifs (JFLA), Pontarlier (France), Jan 2001, X, France. 2001. <hal-01125071>
  • David Delahaye. A Tactic Language for the System Coq. Proceedings of Logic for Programming and Automated Reasoning (LPAR), Reunion Island (France), Jan 2000, X, France. 1955, pp.85-95, 2000, LNCS/LNAI. <hal-01125070>
  • David Delahaye, Roberto Di Cosmo, Benjamin Werner. Recherche dans une bibliothèque de preuves Coq en utilisant le type et modulo isomorphismes. PRC/GDR de programmation, Pôle Preuves et Spécifications Algébriques, Jan 1997, X, France. 1997. <hal-01124982>

Direction d'ouvrage, Proceedings2 documents

  • David Delahaye, Catherine Dubois. Proceedings of the first workshop about Sets and Tools, SETS 2014, affiliated to ABZ 2014. Informal proceedings. 2014. <hal-01126518>
  • David Delahaye, Renaud Rioboo, Serge Autexier, Jacques Calmet, Patrick D. F. Ion, et al.. 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. Springer. 2010. <hal-01126050>

Pré-publication, Document de travail1 document

  • 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. 16 pages. 2005. <hal-00009425>

Rapport1 document

  • David Delahaye. Search2: un outil de recherche dans une bibliothèque de preuves Coq modulo isomorphismes. [Research Report] CEDRIC-97-730, CEDRIC Lab/CNAM. 1997. <hal-01124981>