Documentation
Français (FR)

Anglais (EN)

David Delahaye

13

Documents

Identifiants chercheurs

david-delahaye
0000-0003-4779-1359
IdRef : 082035970

Présentation

Publications

"catherine-dubois"

	BCARe : un environnement pour la vériﬁcation de règles de l'Atelier B Karim Berkani , David Delahaye , Catherine Dubois , Mélanie Jacquel , Martin Keogh Approches Formelles dans l'Assistance au Développement de Logiciels, 2012, pp.46-49 Article dans une revue hal-00722385v1
	Verifying B Proof Rules using Deep Embedding and Automated Theorem Proving Mélanie Jacquel , Karim Berkani , David Delahaye , Catherine Dubois Software Engineering and Formal Methods, 2011, 7041, pp.253-268. ⟨10.1007/978-3-642-24690-6_18⟩ Article dans une revue hal-00722373v1

	Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system Ali Assaf , Guillaume Burel , Raphal Cauderlier , David Delahaye , Gilles Dowek TYPES: Types for Proofs and Programs, May 2016, Novi SAd, Serbia Communication dans un congrès hal-01441751v1
	The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations David Delahaye , Catherine Dubois , Claude Marché , David Mentré Abstract State Machines, Alloy, B, VDM, and Z, Jun 2014, Toulouse, France. pp.290-293 Communication dans un congrès hal-00998092v1
	RelExt : Synthèse de code à partir de spécifications inductives David Delahaye , Catherine Dubois , Pierre-Nicolas Tollitte AFADL 2013, Apr 2013, Nancy, France. 4 p Communication dans un congrès hal-01126320v1
	Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover Mélanie Jacquel , Karim Berkani , David Delahaye , Catherine Dubois International Joint Conference on Automated Reasoning (IJCAR 2012), Jun 2012, Manchester, Ukraine. pp.332--338 Communication dans un congrès hal-01126134v1
	BCARe : un environnement pour la vérification de règles de l?Atelier B Karim Berkani , David Delahaye , Catherine Dubois , Mélanie Jacquel , Martin Keogh Approches Formelles dans l'Assistance au D?veloppement de Logiciels (AFADL 2012), Jan 2012, Grenoble, France. pp.46-49 Communication dans un congrès hal-01126033v1
	Producing Certified Functional Code from Inductive Specifications Pierre-Nicolas Tollitte , David Delahaye , Catherine Dubois International Conference on Certified Programs and Proofs (CPP 2012), Dec 2012, Kyoto, Japan. pp.76-91 Communication dans un congrès hal-01126212v1
	Tableaux Modulo Theories Using Superdeduction Mélanie Jacquel , Karim Berkani , David Delahaye , Catherine Dubois IJCAR 2012 - 6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, UK, United Kingdom. pp.1 - 13, ⟨10.1007/978-3-642-31365-3_26⟩ Communication dans un congrès hal-01099338v1
	Génération de code fonctionnel certifié à partir de spécifications inductives dans l'environnement Focalize David Delahaye , Catherine Dubois , Pierre-Nicolas Tollitte Journ?es Francophones des Langages Applicatifs (JFLA'10), Jan 2010, La Ciotat, France. pp.55-81 Communication dans un congrès hal-01125723v1
	Trusted Software within Focal Philippe Ayrault , Matthieu Carlier , David Delahaye , Catherine Dubois , Damien Doligez C&ESAR 2008 - Computer & Electronics Security Applications Rendez-vous, Dec 2008, Rennes, France. pp.162-179 Communication dans un congrès hal-01125667v2
	Extracting Purely Functional Contents from Logical Inductive Types David Delahaye , Catherine Dubois , Jean-Frédéric Etienne TPHOLs'07 Theorem Proving in Higher Order Logics, Kaiserslautern (Germany), Jan 2007, X, France. pp.70-85 Communication dans un congrès hal-01125370v1

	Proceedings of the first workshop about Sets and Tools, SETS 2014, affiliated to ABZ 2014 David Delahaye , Catherine Dubois Informal proceedings. 2014 Ouvrages hal-01126518v1