2012

Conférence Internationale avec comité de lecture

• [TDD12

  @inproceedings {
  	TDD12,
  	title	=	"{Producing Certified Functional Code from Inductive Specifications}",
  	author	=	" P. Tollitte and D. Delahaye and C. Dubois ",
  	booktitle	=	"{International Conference on Certified Programs and Proofs (CPP 2012)}",
  	year	=	2012,
  	edition	=	"Springer",
  	month	=	"December",
  	series	=	"LNCS",
  	pages	=	"à paraitre",
  	address	=	"Kyoto, Japan",
  }

  ] P. Tollitte , D. Delahaye , C. Dubois - Producing Certified Functional Code from Inductive Specifications, International Conference on Certified Programs and Proofs (CPP 2012), December 2012, pp.à paraitre, Series LNCS, Kyoto, Japan,
• [JBD12

  @inproceedings {
  	JBD12,
  	title	=	"{Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover}",
  	author	=	" M. Jacquel and K. Berkani and D. Delahaye and C. Dubois ",
  	booktitle	=	"{International Joint Conference on Automated Reasoning (IJCAR 2012)}",
  	year	=	2012,
  	month	=	"June",
  	series	=	"LNAI",
  	volume	=	7364,
  	pages	=	"332--338",
  	address	=	"Manchester, UK",
  }

  ] M. Jacquel , K. Berkani , D. Delahaye , C. 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), June 2012, Vol. 7364, pp.332--338, Series LNAI, Manchester, UK,

Conférence Nationale avec comité de lecture

• [BDD12

  @inproceedings {
  	BDD12,
  	title	=	"{BCARe : un environnement pour la vérification de règles de l’Atelier B }",
  	author	=	" K. Berkani and D. Delahaye and C. Dubois and M. Jacquel and M. Keogh and E. Le Lay ",
  	booktitle	=	"{Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL 2012)}",
  	year	=	2012,
  	month	=	"January",
  	pages	=	"46-49",
  	address	=	"Grenoble, France",
  }

  ] K. Berkani , D. Delahaye , C. Dubois , M. Jacquel , M. Keogh , E. Le Lay - 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), January 2012, pp.46-49, Grenoble, France,

2011

Conférence Internationale avec comité de lecture

• [JBD11

  @inproceedings {
  	JBD11,
  	title	=	"{Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving.}",
  	author	=	" M. Jacquel and K. Berkani and D. Delahaye and C. Dubois ",
  	booktitle	=	"{Software Engineering and Formal Methods - 9th International Conference, SEFM 2011}",
  	year	=	2011,
  	month	=	"November",
  	series	=	"LNCS",
  	volume	=	7041,
  	pages	=	"253-268",
  	address	=	"Montevideo, Uruguay",
  }

  ] M. Jacquel , K. Berkani , D. Delahaye , C. Dubois - Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving., Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, November 2011, Vol. 7041, pp.253-268, Series LNCS, Montevideo, Uruguay,

2010

Conférence Nationale avec comité de lecture

• [DDT10

  @inproceedings {
  	DDT10,
  	title	=	"{Génération de code fonctionnel certifié à partir de spécifications inductives dans l'environnement Focalize}",
  	author	=	" D. Delahaye and C. Dubois and P. Tollitte ",
  	booktitle	=	"{ Journées Francophones des Langages Applicatifs (JFLA'10)}",
  	year	=	2010,
  	month	=	"January",
  	series	=	"Studia informatica universalis ",
  	pages	=	"55-81",
  	address	=	"La Ciotat , 0",
  	note	=	"{note}",
  }

  ] D. Delahaye , C. Dubois , P. 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), January 2010, pp.55-81, Series Studia informatica universalis , La Ciotat ,

Directions d'ouvrages scientifiques

• [DRA10

  @book {
  	DRA10,
  	title	=	"{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}",
  	author	=	"D. Delahaye and R. Rioboo and S. Autexier and J. Calmet and P. Ion and L. Rideau and A. Sexton",
  	year	=	2010,
  	publisher	=	"Springer",
  }

  ] D. Delahaye , R. Rioboo , S. Autexier , J. Calmet , P. Ion , L. Rideau , A. 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, July 2010, Springer,

Mémoire de HDR

• [Del10

  @misc {
  	Del10,
  	title	=	"{Assisting Users of Proof Assistants}",
  	author	=	"D. Delahaye",
  	year	=	2010,
  	address	=	"{CEDRIC Laboratory, Paris, France}",
  	note	=	"{Post-Doctoral Degree (Phd students supervisor) Directeur: Rapporteur 1: Rapporteur 2: Membre du jury: Membre du jury: Membre du jury:}",
  }

  ] D. Delahaye - Assisting Users of Proof Assistants, Soutenue le: 09 December 2010,

2008

Conférence Internationale avec comité de lecture

• [DEV08a

  @inproceedings {
  	DEV08a,
  	title	=	"{Producing UML Models from Focal Specifications: An Application to Airport Security Regulations}",
  	author	=	" D. Delahaye and J. Etienne and V. Viguie Donzeau-Gouge ",
  	booktitle	=	"{TASE'08 Theoretical Aspects of Software Engineering, Nanjing (China)}",
  	year	=	2008,
  	edition	=	"IEEE CS Press",
  	month	=	"January",
  	pages	=	"121-124",
  }

  ] D. Delahaye , J. Etienne , V. Viguie Donzeau-Gouge - Producing UML Models from Focal Specifications: An Application to Airport Security Regulations, TASE'08 Theoretical Aspects of Software Engineering, Nanjing (China), January 2008, pp.121-124,
• [DEV08b

  @inproceedings {
  	DEV08b,
  	title	=	"{Formal Modeling of Airport Security Regulations using the Focal Environment}",
  	author	=	" D. Delahaye and J. Etienne and V. Viguie Donzeau-Gouge ",
  	booktitle	=	"{RELAW'08 Requirements Engineering and Law, Barcelona (Spain)}",
  	year	=	2008,
  	edition	=	"IEEE CS Press",
  	month	=	"January",
  	pages	=	"16-20",
  }

  ] D. Delahaye , J. Etienne , V. Viguie Donzeau-Gouge - Formal Modeling of Airport Security Regulations using the Focal Environment, RELAW'08 Requirements Engineering and Law, Barcelona (Spain), January 2008, pp.16-20,
• [DEV08

  @inproceedings {
  	DEV08,
  	title	=	"{A Formal and Sound Transformation from Focal to UML: An Application to Airport Security Regulations}",
  	author	=	" D. Delahaye and J. Etienne and V. Viguie Donzeau-Gouge ",
  	booktitle	=	"{UML&FM'08 UML and Formal Methods, Kitakyushu-City (Japan)}",
  	year	=	2008,
  	month	=	"January",
  	series	=	"ISSE",
  	volume	=	4,
  	pages	=	"267-274",
  }

  ] D. Delahaye , J. Etienne , V. Viguie Donzeau-Gouge - A Formal and Sound Transformation from Focal to UML: An Application to Airport Security Regulations, UML&FM'08 UML and Formal Methods, Kitakyushu-City (Japan), January 2008, Vol. 4, pp.267-274, Series ISSE,

Conférence Nationale avec comité de lecture

• [ACD08

  @inproceedings {
  	ACD08,
  	title	=	"{Trusted Software within FoCaL}",
  	author	=	" P. Ayrault and M. Carlier and D. Delahaye and C. Dubois and D. Doligez and L. Habib and T. Hardin and M. Jaume and C. Morisset and F. Pessaux and P. Weis ",
  	booktitle	=	"{CE&SAR 2008, Rennes, décembre}",
  	year	=	2008,
  	month	=	"December",
  	pages	=	"142-157",
  	note	=	"{note}",
  }

  ] P. Ayrault , M. Carlier , D. Delahaye , C. Dubois , D. Doligez , L. Habib , T. Hardin , M. Jaume , C. Morisset , F. Pessaux , P. Weis - Trusted Software within FoCaL, CE&SAR 2008, Rennes, décembre, December 2008, pp.142-157,

2007

Conférence Internationale avec comité de lecture

• [DDE07

  @inproceedings {
  	DDE07,
  	title	=	"{Extracting Purely Functional Contents from Logical Inductive Types}",
  	author	=	" D. Delahaye and C. Dubois and J. Etienne ",
  	booktitle	=	"{TPHOLs'07 Theorem Proving in Higher Order Logics, Kaiserslautern (Germany)}",
  	year	=	2007,
  	month	=	"January",
  	series	=	"LNCS",
  	volume	=	4732,
  	pages	=	"70-85",
  }

  ] D. Delahaye , C. Dubois , J. Etienne - Extracting Purely Functional Contents from Logical Inductive Types, TPHOLs'07 Theorem Proving in Higher Order Logics, Kaiserslautern (Germany), January 2007, Vol. 4732, pp.70-85, Series LNCS,
• [BDD07

  @inproceedings {
  	BDD07,
  	title	=	"{Zenon: an Extensible Automated Theorem Prover Producing Checkable Proofs}",
  	author	=	" R. Bonichon and D. Delahaye and D. Doligez ",
  	booktitle	=	"{LPAR'07 Logic for Programming Artificial Intelligence and Reasoning, Yerevan (Armenia)}",
  	year	=	2007,
  	month	=	"January",
  	series	=	"LNAI",
  	pages	=	"151-165",
  }

  ] R. Bonichon , D. Delahaye , D. Doligez - Zenon: an Extensible Automated Theorem Prover Producing Checkable Proofs, LPAR'07 Logic for Programming Artificial Intelligence and Reasoning, Yerevan (Armenia), January 2007, pp.151-165, Series LNAI,

2006

Conférence Internationale avec comité de lecture

• [DEV06b

  @inproceedings {
  	DEV06b,
  	title	=	"{Modeling Airport Security Regulations in Focal}",
  	author	=	" D. Delahaye and J. Etienne and V. Viguie Donzeau-Gouge ",
  	booktitle	=	"{REMO2V'06 Regulations Modelling and their Validation & Verification, Luxembourg}",
  	year	=	2006,
  	month	=	"January",
  	pages	=	"806-812",
  }

  ] D. Delahaye , J. Etienne , V. Viguie Donzeau-Gouge - Modeling Airport Security Regulations in Focal, REMO2V'06 Regulations Modelling and their Validation & Verification, Luxembourg, January 2006, pp.806-812,
• [DEV06

  @inproceedings {
  	DEV06,
  	title	=	"{Certifying Airport Security Regulations using the Focal Environment}",
  	author	=	" D. Delahaye and J. Etienne and V. Viguie Donzeau-Gouge ",
  	booktitle	=	"{FM'06: 14th Symposium on Formal Methods, Hamilton, Canada}",
  	year	=	2006,
  	month	=	"January",
  	series	=	"LNCS",
  	volume	=	4085,
  	pages	=	"48-63",
  }

  ] D. Delahaye , J. Etienne , V. Viguie Donzeau-Gouge - Certifying Airport Security Regulations using the Focal Environment, FM'06: 14th Symposium on Formal Methods, Hamilton, Canada, January 2006, Vol. 4085, pp.48-63, Series LNCS,
• [DEV06a

  @inproceedings {
  	DEV06a,
  	title	=	"{Reasoning about Airport Security Regulations using the Focal Environment}",
  	author	=	" D. Delahaye and J. Etienne and V. Viguie Donzeau-Gouge ",
  	booktitle	=	"{ISoLA, Paphos (Cyprus)}",
  	year	=	2006,
  	month	=	"January",
  	pages	=	"36-44",
  }

  ] D. Delahaye , J. Etienne , V. Viguie Donzeau-Gouge - Reasoning about Airport Security Regulations using the Focal Environment, ISoLA, Paphos (Cyprus), January 2006, pp.36-44,

2005

Revue Internationale avec comité de lecture

• [DM05

  @article {
  	DM05,
  	title	=	"{Dealing with Algebraic Expressions over a Field in Coq using Maple}",
  	author	=	"D. Delahaye and M. Mayero",
  	journal	=	"JSC'05 J. of Symbolic Computation",
  	year	=	2005,
  	volume	=	39,
  	number	=	5,
  	pages	=	"569-592",
  }

  ] D. Delahaye , M. Mayero - Dealing with Algebraic Expressions over a Field in Coq using Maple, JSC'05 J. of Symbolic Computation, vol. 39(5), pp. 569-592, 2005

Revue Nationale avec comité de lecture

• [DJP05

  @article {
  	DJP05,
  	title	=	"{Coq: un outil pour l'enseignement}",
  	author	=	"D. Delahaye and M. Jaume and V. Prevosto",
  	journal	=	"TSI, Technique et Science Informatiques",
  	year	=	2005,
  	volume	=	24,
  	number	=	9,
  	pages	=	"1139-1160",
  }

  ] D. Delahaye , M. Jaume , V. Prevosto - Coq: un outil pour l'enseignement, TSI, Technique et Science Informatiques, vol. 24(9), pp. 1139-1160, 2005

Conférence Internationale avec comité de lecture

• [DM05a

  @inproceedings {
  	DM05a,
  	title	=	"{Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System}",
  	author	=	" D. Delahaye and M. Mayero ",
  	booktitle	=	"{Calculemus, University of Newcastle upon Tyn (United Kingdom)}",
  	year	=	2005,
  	month	=	"January",
  	series	=	"ENTCS",
  	volume	=	151,
  	issue	=	1,
  	pages	=	"57-73",
  }

  ] D. Delahaye , M. Mayero - Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System, Calculemus, University of Newcastle upon Tyn (United Kingdom), January 2005, Vol. 151(1), pp.57-73, Series ENTCS,

2002

Conférence Internationale avec comité de lecture

• [DEL02

  @inproceedings {
  	DEL02,
  	title	=	"{A Proof Dedicated Meta-Language}",
  	author	=	" D. Delahaye ",
  	booktitle	=	"{Proceedings of Logical Frameworks and Meta-Languages (LFM), Copenhagen (Denmark)}",
  	year	=	2002,
  	month	=	"January",
  	series	=	"ENTCS",
  	volume	=	70,
  	issue	=	2,
  }

  ] D. Delahaye - A Proof Dedicated Meta-Language, Proceedings of Logical Frameworks and Meta-Languages (LFM), Copenhagen (Denmark), January 2002, Vol. 70(2), Series ENTCS,
• [DEL02a

  @inproceedings {
  	DEL02a,
  	title	=	"{Free-style Theorem Proving}",
  	author	=	" D. Delahaye ",
  	booktitle	=	"{Proceedings of Theorem Proving in Higher Order Logics (TPHOLs), Hampton (VA, USA)}",
  	year	=	2002,
  	month	=	"January",
  	series	=	"LNCS",
  	volume	=	2410,
  	pages	=	"164-181",
  }

  ] D. Delahaye - Free-style Theorem Proving, Proceedings of Theorem Proving in Higher Order Logics (TPHOLs), Hampton (VA, USA), January 2002, Vol. 2410, pp.164-181, Series LNCS,

2001

Conférence Nationale avec comité de lecture

• [DM01

  @inproceedings {
  	DM01,
  	title	=	"{Field: une procédure de décision pour les nombres réels en Coq}",
  	author	=	" D. Delahaye and M. Mayero ",
  	booktitle	=	"{Journées Francophones des Langages Applicatifs (JFLA), Pontarlier (France)}",
  	year	=	2001,
  	month	=	"January",
  }

  ] D. Delahaye , M. Mayero - Field: une procédure de décision pour les nombres réels en Coq, Journées Francophones des Langages Applicatifs (JFLA), Pontarlier (France), January 2001,

Mémoire de Thèse

• [DEL01

  @phdthesis {
  	DEL01,
  	title	=	"{Conception de langages pour décrire les preuves et les automatisations dans les outils d'aide à la preuve: une étude dans le cadre du système Coq}",
  	author	=	"D. Delahaye",
  	year	=	2001,
  	address	=	"{CEDRIC Laboratory, Paris, France}",
  	note	=	"{note}",
  }

  ] D. Delahaye - Conception de langages pour décrire les preuves et les automatisations dans les outils d'aide à la preuve: une étude dans le cadre du système Coq, Soutenue le: 01 January 2001,

2000

Conférence Internationale avec comité de lecture

• [DEL00

  @inproceedings {
  	DEL00,
  	title	=	"{A Tactic Language for the System Coq}",
  	author	=	" D. Delahaye ",
  	booktitle	=	"{Proceedings of Logic for Programming and Automated Reasoning (LPAR), Reunion Island (France)}",
  	year	=	2000,
  	month	=	"January",
  	series	=	"LNCS/LNAI",
  	volume	=	1955,
  	pages	=	"85-95",
  }

  ] D. Delahaye - A Tactic Language for the System Coq, Proceedings of Logic for Programming and Automated Reasoning (LPAR), Reunion Island (France), January 2000, Vol. 1955, pp.85-95, Series LNCS/LNAI,

1999

Conférence Internationale avec comité de lecture

• [DEL99

  @inproceedings {
  	DEL99,
  	title	=	"{Information Retrieval in a Coq Proof Library using Type Isomorphisms}",
  	author	=	" D. Delahaye ",
  	year	=	1999,
  	month	=	"January",
  	volume	=	1956,
  	pages	=	"131-147",
  }

  ] D. Delahaye - Information Retrieval in a Coq Proof Library using Type Isomorphisms, January 1999, Vol. 1956, pp.131-147,

1997

Conférence Nationale avec comité de lecture

• [DDW97

  @inproceedings {
  	DDW97,
  	title	=	"{ Recherche dans une bibliothèque de preuves Coq en utilisant le type et modulo isomorphismes}",
  	author	=	" D. Delahaye and R. Di Cosmo and B. Werner ",
  	booktitle	=	"{PRC/GDR de programmation, Pôle Preuves et Spécifications Algébriques}",
  	year	=	1997,
  	month	=	"January",
  	note	=	"{note}",
  }

  ] D. Delahaye , R. Di Cosmo , B. 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, January 1997,

Rapport Scientifique

• [DEL97

  @techreport {
  	DEL97,
  	title	=	"{Search2: un outil de recherche dans une bibliothèque de preuves Coq modulo isomorphismes}",
  	author	=	"D. Delahaye",
  	number	=	"{CEDRIC-97-730}",
  	institution	=	"{CEDRIC laboratory, CNAM-Paris, France}",
  	date	=	{01-01-1997},
  	note	=	"{Rapport du DEA Sémantique, Preuves et Programmation, Université Pierre et Marie Curie (Paris 6).}",
  }

  ] D. Delahaye - Search2: un outil de recherche dans une bibliothèque de preuves Coq modulo isomorphismes, Date de dépot: 1997/01/01, (Tech. Rep.: CEDRIC-97-730)