Publications
2014
- Mélanie Jacquel, Karim Berkani, David Delahaye, and Catherine Dubois.
Tableaux Modulo Theories using Superdeduction. Global Journal of Advanced
Software Engineering (GJASE), 1:1—13, December 2014.
PDF
@article{Tab-Sded2,
author = "Jacquel, Mélanie and Berkani, Karim and Delahaye, David and Dubois, Catherine",
title = "{Tableaux Modulo Theories using Superdeduction}",
journal = "Global Journal of Advanced Software Engineering (GJASE)",
volume = 1,
pages = "1--13",
month = dec,
year = 2014
} - David Delahaye, Claude Marché, and David Mentré. Le projet BWare: une
plate-forme pour la vérification automatique d'obligations de preuve B. In
Catherine Dubois and Régine Laleau, editors, Approches Formelles dans
l'Assistance au Développement de Logiciels (AFADL), pages 126—127,
Paris (France), June 2014.
PDF
@inproceedings{BWare2,
author = "Delahaye, David and Marché, Claude and Mentré, David",
title = "{Le projet \textsf{BWare}: une plate-forme pour la vérification automatique d'obligations de preuve B}",
booktitle = "Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL)",
editor = "Dubois, Catherine and Laleau, Régine",
address = "Paris (France)",
pages = "126--127",
month = jun,
year = 2014
} - David Delahaye, Catherine Dubois, Claude Marché, and David Mentré.
The BWare Project: Building a Proof Platform for the Automated Verification of B
Proof Obligations. In Yamine Ait Ameur and Klaus-Dieter Schewe, editors,
Abstract State Machines, Alloy, B, VDM, and Z (ABZ), Lecture Notes in
Computer Science (LNCS), Toulouse (France), June 2014. Springer. To appear.
PDF
@inproceedings{BWare,
author = "Delahaye, David and Dubois, Catherine and Marché, Claude and Mentré, David",
title = "{The \textsf{BWare} Project: Building a Proof Platform for the Automated Verification of \textsf{B} Proof Obligations}",
booktitle = "Abstract State Machines, \textsf{Alloy}, \textsf{B}, \textsf{VDM}, and \textsf{Z} (ABZ)",
editor = "Ait~Ameur, Yamine and Schewe, Klaus-Dieter",
publisher = "Springer",
series = "Lecture Notes in Computer Science (LNCS)",
address = "Toulouse (France)",
month = jun,
year = 2014,
note = "To appear"
}
2013
- David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and
Olivier Hermant. Zenon Modulo: When Achilles Outruns the Tortoise using
Deduction Modulo. In Ken McMillan, Aart Middeldorp, and Voronkov Andrei,
editors, Logic for Programming Artificial Intelligence and Reasoning
(LPAR), volume 8312 of Lecture Notes in Computer Science (LNCS)/Advanced
Research in Computing and Software Science (ARCoSS), pages 274—290,
Stellenbosch (South Africa), December 2013. Springer.
PDF
@inproceedings{Zenon-Modulo,
author = "Delahaye, David and Doligez, Damien and Gilbert, Frédéric and Halmagrand, Pierre and Hermant, Olivier",
title = "{\textsf{Zenon~Modulo}: When Achilles Outruns the Tortoise using Deduction Modulo}",
booktitle = "Logic for Programming Artificial Intelligence and Reasoning (LPAR)",
editor = "McMillan, Ken and Middeldorp, Aart and Voronkov Andrei",
publisher = "Springer",
series = "Lecture Notes in Computer Science (LNCS)/Advanced Research in Computing and Software Science (ARCoSS)",
address = "Stellenbosch (South Africa)",
volume = 8312,
pages = "274--290",
month = dec,
year = 2013
} - David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and
Olivier Hermant. Proof Certification in Zenon Modulo: When Achilles Uses
Deduction Modulo to Outrun the Tortoise with Shorter Steps. In Ken McMillan,
Aart Middeldorp, and Voronkov Andrei, editors, International Workshop on the
Implementation of Logics (IWIL), Stellenbosch (South Africa), December
2013. EasyChair. To appear.
PDF
@inproceedings{Zenon-Modulo2, author = "Delahaye, David and Doligez, Damien and Gilbert, Frédéric and Halmagrand, Pierre and Hermant, Olivier",
title = "{Proof Certification in \textsf{Zenon~Modulo}: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps}",
booktitle = "International Workshop on the Implementation of Logics (IWIL)",
editor = "McMillan, Ken and Middeldorp, Aart and Voronkov Andrei",
publisher = "EasyChair",
address = "Stellenbosch (South Africa)",
month = dec,
year = 2013,
note = "To appear"
} - Mélanie Jacquel, Karim Berkani, David Delahaye, and Catherine Dubois.
Verifying B Proof Rules using Deep Embedding and Automated Theorem Proving.
Software and Systems Modeling (SoSyM), June 2013. To appear.
PDF
@article{B2Zenon,
author = "Jacquel, Mélanie and Berkani, Karim and Delahaye, David and Dubois, Catherine",
title = "{Verifying \textsf{B} Proof Rules using Deep Embedding and Automated Theorem Proving}",
journal = "Software and Systems Modeling (SoSyM)",
month = jun,
year = 2013,
note = "To appear"
} - David Delahaye and Mélanie Jacquel. Recovering Intuition from Automated
Formal Proofs using Tableaux with Superdeduction. Electronic Journal of
Mathematics and Technology (eJMT), 7(2), February 2013.
PDF
@article{Super-Zenon,
author = "Delahaye, David and Jacquel, Mélanie",
title = "{Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction}",
journal = "Electronic Journal of Mathematics and Technology (eJMT)",
volume = 7,
number = 2,
month = feb,
year = 2013
} Cited by
2012
- Pierre-Nicolas Tollitte, David Delahaye, and Catherine Dubois. Producing
Certified Functional Code from Inductive Specifications. In Chris Hawblitzel and
Dale Miller, editors, Certified Programs and Proofs (CPP), volume 7679 of
Lecture Notes in Computer Science (LNCS), pages 76—91, Kyoto
(Japan), December 2012. Springer.
PDF
@inproceedings{Rel-Exec3,
author = "Tollitte, Pierre-Nicolas and Delahaye, David and Dubois, Catherine",
title = "{Producing Certified Functional Code from Inductive Specifications}",
booktitle = "Certified Programs and Proofs (CPP)",
editor = "Hawblitzel, Chris and Miller, Dale",
publisher = "Springer",
series = "Lecture Notes in Computer Science (LNCS)", address = "Kyoto (Japan)",
volume = 7679,
pages = "76--91",
month = dec,
year = 2012
} - Mélanie Jacquel, Karim Berkani, David Delahaye, and Catherine Dubois.
Tableaux Modulo Theories using Superdeduction: An Application to the
Verification of B Proof Rules with the Zenon Automated Theorem Prover. In
Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, International Joint
Conference on Automated Reasoning (IJCAR), volume 7364 of Lecture Notes
in Computer Science (LNCS), pages 332—338, Manchester (UK), June
2012. Springer.
PDF
@inproceedings{Tab-Sded,
author = "Jacquel, Mélanie and Berkani, Karim and Delahaye, David and Dubois, Catherine",
title = "{Tableaux Modulo Theories using Superdeduction: An Application to the Verification of \textsf{B} Proof Rules with the \textsf{Zenon} Automated Theorem Prover}",
booktitle = "International Joint Conference on Automated Reasoning (IJCAR)",
editor = "Gramlich, Bernhard and Miller, Dale and Sattler, Uli",
publisher = "Springer",
series = "Lecture Notes in Computer Science (LNCS)",
address = "Manchester (UK)",
volume = 7364,
pages = "332--338",
month = jun,
year = 2012
} Cited by
2011
- Mélanie Jacquel, Karim Berkani, David Delahaye, and Catherine Dubois.
Verifying B Proof Rules using Deep Embedding and Automated Theorem Proving. In
Gilles Barthe, Alberto Pardo, and Gerardo Schneider, editors, Software
Engineering and Formal Methods (SEFM), volume 7041 of Lecture Notes in
Computer Science (LNCS), pages 253—268. Springer, 2011.
PDF
@inproceedings{B2Zenon2,
author = "Jacquel, Mélanie and Berkani, Karim and Delahaye, David and Dubois, Catherine",
title = "{Verifying \textsf{B} Proof Rules using Deep Embedding and Automated Theorem Proving}",
booktitle = "Software Engineering and Formal Methods (SEFM)",
editor = "Barthe, Gilles and Pardo, Alberto and Schneider, Gerardo",
publisher = "Springer",
series = "Lecture Notes in Computer Science (LNCS)",
address = "Montevideo (Uruguay)",
volume = 7041,
pages = "253--268",
month = nov,
year = 2011
} Cited by
2010
- David Delahaye. Assisting Users of Proof Assistants. HDR thesis, Université
Pierre et Marie Curie (Paris 6), December 2010.
PDF
@misc{HDR-Thesis,
author = "Delahaye, David",
title = "{Assisting Users of Proof Assistants}",
howpublished = "HDR thesis, Université Pierre et Marie~Curie (Paris~6)",
month = dec,
year = 2010
} - Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence
Rideau, Renaud Rioboo, and Alan P. Sexton, editors. 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, volume 6167 of Lecture Notes in Computer Science
(LNCS), Paris (France), July 2010. Springer. ISBN 978-3-642-14127-0.
The proceedings are available at www.springerlink.com.
@proceedings{CICM2010,
editor = "Autexier, Serge and Calmet, Jacques and Delahaye, David and Ion, Patrick D. F. and Rideau, Laurence and Rioboo, Renaud and Sexton, Alan P.",
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",
publisher = "Springer",
series = "Lecture Notes in Computer Science (LNCS)",
address = "Paris (France)",
volume = 6167,
month = jul,
year = 2010,
note = "ISBN 978-3-642-14127-0"
} - The Focalize Development Team. Focalize, version 0.6.0. Cnam, Inria,
and LIP6, May 2010.
http://focalize.inria.fr/.
@manual{Focalize,
author = "{The \textsf{Focalize} Development Team}",
title = "\textsf{Focalize}, version~0.6.0",
organization = "\textsf{Cnam}, \textsf{Inria}, and \textsf{LIP6}",
month = may,
year = 2010,
note = "\url{http://focalize.inria.fr/}"
}
- David Delahaye, Catherine Dubois, and Pierre-Nicolas Tollitte. Génération de
code fonctionnel certifié à partir de spécifications inductives dans
l'environnement Focalize. In Sylvain Conchon and Micaela Mayero, editors,
Journées Francophones des Langages Applicatifs (JFLA), Vieux-Port La
Ciotat (France), January 2010. Inria.
The original publication is available at jfla.inria.fr.
PDF
@inproceedings{Rel-Exec2,
author = "Delahaye, David and Dubois, Catherine and Tollitte, Pierre-Nicolas",
title = "Génération de code fonctionnel certifié à partir de spécifications inductives dans l'environnement \textsf{Focalize}",
booktitle = "Journées Francophones des Langages Applicatifs (JFLA)",
editor = "Conchon, Sylvain and Mayero, Micaela",
publisher = "\textsf{Inria}",
address = "Vieux-Port La Ciotat (France)",
month = jan,
year = 2010
}
2009
- Nicolas Bertaux and David Delahaye. Developing Structured Libraries using
the Focal Environment. In Florian Rabe and Carsten Schuermann, editors,
Modules and Libraries for Proof Assistants (MLPA), volume 429, pages
2–10, Montréal (Canada), August 2009. ACM Press.
PDF
@inproceedings{Focal-Mod,
author = "Bertaux, Nicolas and Delahaye, David", title = "{Developing Structured Libraries using the \textsf{Focal} Environment}",
booktitle = "Modules and Libraries for Proof Assistants (MLPA)",
editor = "Rabe, Florian and Schuermann, Carsten",
publisher = "ACM Press",
address = "Montréal (Canada)",
volume = 429,
pages = "2--10",
month = aug,
year = 2009
}
2008
- David Delahaye, Jean-Frédéric Étienne, and Véronique Viguié~Donzeau-Gouge. A
Formal and Sound Transformation from Focal to UML: An Application to Airport
Security Regulations. Innovations in Systems and Software Engineering (ISSE)
NASA Journal, 4(3):267–274,
September 2008.
PDF
@article{Focal-UML,
author = "Delahaye, David and Étienne, Jean-Frédéric and Viguié~Donzeau-Gouge, Véronique",
title = "{A Formal and Sound Transformation from \textsf{Focal} to \textsf{UML}: An Application to Airport Security Regulations}",
journal = "Innovations in Systems and Software Engineering (ISSE) \textsf{NASA} Journal",
volume = 4,
number = 3,
pages = "267--274",
month = sep,
year = 2008
}
Cited by - David Delahaye, Jean-Frédéric Étienne, and Véronique Viguié Donzeau-Gouge.
Formal Modeling of Airport Security Regulations using the Focal Environment. In
Travis Breaux and John Mylopoulos, editors, Requirements Engineering and Law
(RELAW), pages 16—20, Barcelona (Spain), September 2008. IEEE CS
Press.
PDF
@inproceedings{EDEMOI-All2,
author = "Delahaye, David and Étienne, Jean-Frédéric and Viguié Donzeau-Gouge, Véronique",
title = "{Formal Modeling of Airport Security Regulations using the \textsf{Focal} Environment}",
booktitle = "Requirements Engineering and Law (RELAW)",
editor = "Breaux, Travis and Mylopoulos, John",
publisher = "IEEE CS Press",
address = "Barcelona (Spain)",
pages = "16--20",
month = sep,
year = 2008
}
Cited by - David Delahaye, Jean-Frédéric Étienne, and Véronique Viguié~Donzeau-Gouge.
Producing UML Models from Focal Specifications: An Application to Airport
Security Regulations. In Jim Davies, Jifeng He, Xuandong Li, and Jian Lu,
editors, Theoretical Aspects of Software Engineering (TASE), pages
121—124, Nanjing (China), June 2008. IEEE CS Press.
PDF
@inproceedings{Focal-UML2,
author = "Delahaye, David and Étienne, Jean-Frédéric and Viguié~Donzeau-Gouge, Véronique",
title = "{Producing \textsf{UML} Models from \textsf{Focal} Specifications: An Application to Airport Security Regulations}",
booktitle = "Theoretical Aspects of Software Engineering (TASE)",
editor = "Davies, Jim and He, Jifeng and Li, Xuandong and Lu, Jian",
publisher = "IEEE CS Press",
address = "Nanjing (China)",
pages = "121--124",
month = jun,
year = 2008
}
Cited by
2007
- Richard Bonichon, David Delahaye, and Damien Doligez. Zenon: An Extensible
Automated Theorem Prover Producing Checkable Proofs. In Nachum Dershowitz and
Andrei Voronkov, editors, Logic for Programming Artificial Intelligence and
Reasoning (LPAR), volume 4790 of Lecture Notes in Computer Science
(LNCS)/Lecture Notes in Artificial Intelligence (LNAI), pages 151—165,
Yerevan (Armenia), October 2007. Springer.
The original publication is available at www.springerlink.com.
PDF
@inproceedings{Zenon,
author = "Bonichon, Richard and Delahaye, David and Doligez, Damien",
title = "{\textsf{Zenon}: An Extensible Automated Theorem Prover Producing Checkable Proofs}",
booktitle = "Logic for Programming Artificial Intelligence and Reasoning (LPAR)",
editor = "Dershowitz, Nachum and Voronkov, Andrei",
publisher = "Springer",
series = "Lecture Notes in Computer Science (LNCS)/Lecture Notes in Artificial Intelligence (LNAI)",
address = "Yerevan (Armenia)",
volume = 4790,
pages = "151--165",
month = oct,
year = 2007
}
Cited by - David Delahaye, Catherine Dubois, and Jean-Frédéric Étienne. Extracting
Purely Functional Contents from Logical Inductive Types. In Klaus Schneider and
Jens Brandt, editors, Theorem Proving in Higher Order Logics (TPHOLs),
volume 4732 of Lecture Notes in Computer Science (LNCS), pages
70—85, Kaiserslautern (Germany), September 2007. Springer.
The original publication is available at www.springerlink.com.
PDF
@inproceedings{Rel-Exec,
author = "Delahaye, David and Dubois, Catherine and Étienne, Jean-Frédéric",
title = "{Extracting Purely Functional Contents from Logical Inductive Types}",
booktitle = "Theorem Proving in Higher Order Logics (TPHOLs)",
editor = "Schneider, Klaus and Brandt, Jens",
publisher = "Springer",
series = "Lecture Notes in Computer Science (LNCS)",
address = "Kaiserslautern (Germany)",
volume = 4732,
pages = "70--85",
month = sep,
year = 2007
}
Cited by
2006
- David Delahaye, Jean-Frédéric Étienne, and Véronique Viguié
Donzeau-Gouge. Reasoning about Airport Security Regulations using the Focal
Environment. In Tiziana Margaria, Anna Philippou, and Bernhard Steffen, editors,
International Symposium on Leveraging Applications of Formal Methods,
Verification and Validation (ISoLA), pages 45—52, Paphos (Cyprus),
November 2006.
PDF
@inproceedings{EDEMOI-Proof,
author = "Delahaye, David and Étienne, Jean-Frédéric and Viguié Donzeau-Gouge, Véronique",
title = "{Reasoning about Airport Security Regulations using the \textsf{Focal} Environment}",
booktitle = "International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)",
editor = "Margaria, Tiziana and Philippou, Anna and Steffen, Bernhard",
publisher = "IEEE CS Press",
address = "Paphos (Cyprus)",
pages = "45--52",
month = nov,
year = 2006
}
Cited by - David Delahaye, Jean-Frédéric Étienne, and Véronique Viguié
Donzeau-Gouge. Certifying Airport Security Regulations using the Focal
Environment. In Jayadev Misra, Tobias Nipkow, and Emil Sekerinski, editors,
Formal Methods (FM), volume 4085 of Lecture Notes in Computer Science
(LNCS), pages 48—63, Hamilton (Ontario, Canada), August 2006.
Springer.
The original publication is available at www.springerlink.com.
PDF
@inproceedings{EDEMOI-Model,
author = "Delahaye, David and Étienne, Jean-Frédéric and Viguié Donzeau-Gouge, Véronique",
title = "{Certifying Airport Security Regulations using the \textsf{Focal} Environment}",
booktitle = "Formal Methods (FM)",
editor = "Misra, Jayadev and Nipkow, Tobias and Sekerinski, Emil",
publisher = "Springer",
series = "Lecture Notes in Computer Science (LNCS)",
address = "Hamilton (Ontario, Canada)",
volume = 4085,
pages = "48--63",
month = aug,
year = 2006
}
Cited by - David Delahaye, Jean-Frédéric Étienne, and Véronique Viguié
Donzeau-Gouge. Modeling Airport Security Regulations in Focal. In Régine Laleau
and Michel Lemoine, editors, Regulations Modelling and their Validation &
Verification (REMO2V), as part of the Conference on Advanced Information System
Engineering (CAiSE), pages 806—812, Luxembourg (Grand-Duchy of
Luxembourg), June 2006. Presses Universitaires de Namur.
PDF
@inproceedings{EDEMOI-Model2,
author = "Delahaye, David and Étienne, Jean-Frédéric and Viguié Donzeau-Gouge, Véronique",
title = "{Modeling Airport Security Regulations in \textsf{Focal}}",
booktitle = "Regulations Modelling and their Validation \& Verification (REMO2V)",
editor = "Laleau, Régine and Lemoine, Michel",
publisher = "Presses Universitaires de Namur",
address = "Luxembourg (Grand-Duchy of Luxembourg)",
pages = "806--812",
month = jun,
year = 2006
}
Cited by
2005
- David Delahaye and Micaela Mayero. Diophantus' 20th Problem and Fermat's
Last Theorem for
n = 4: Formalization of Fermat's Proofs in the Coq Proof Assistant. Draft, October 2005.
This draft is available at arXiv.org.
PDF
@misc{Diophante-Fermat,
author = "Delahaye, David and Mayero, Micaela",
title = "{Diophantus' 20th Problem and Fermat's Last Theorem for $n=4$: Formalization of Fermat's Proofs in the \textsf{Coq} Proof Assistant}",
howpublished = "Draft",
month = oct,
year = 2005,
note = "\url{http://arxiv.org/abs/cs/0510011}"
}
Cited by - David Delahaye and Micaela Mayero. Quantifier Elimination over Algebraically
Closed Fields in a Proof Assistant using a Computer Algebra System. In Jacques
Carette and William M. Farmer, editors, Symposium on the Integration of
Symbolic Computation and Mechanized Reasoning (Calculemus), volume 151(1) of
Electronic Notes in Theoretical Computer Science (ENTCS), pages
57—73, University of Newcastle upon Tyn (United Kingdom), July 2005.
Elsevier.
PDF
@inproceedings{QElim,
author = "Delahaye, David and Mayero, Micaela",
title = "{Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System}",
booktitle = "Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus)",
editor = "Carette, Jacques and Farmer, William M.",
publisher = "Elsevier",
series = "Electronic Notes in Theoretical Computer Science (ENTCS)",
address = "University of Newcastle upon Tyn (United Kingdom)",
volume = "151(1)",
pages = "57--73",
month = jul,
year = 2005
}
Cited by - David Delahaye and Micaela Mayero. Dealing with Algebraic Expressions over a
Field in Coq using Maple. Journal of Symbolic Computation (JSC),
39(5):569—592, May 2005.
PDF
@article{Maple-Mode,
author = "Delahaye, David and Mayero, Micaela",
title = "{Dealing with Algebraic Expressions over a Field in \textsf{Coq} using \textsf{Maple}}",
journal = "Journal of Symbolic Computation (JSC)",
volume = 39,
number = 5,
pages = "569--592",
month = may,
year = 2005
}
Cited by - The Focal Development Team. Focal, version 0.3.1. Cnam, Inria, and
LIP6, May 2005. http://focal.inria.fr/.
@manual{Focal,
author = "{The \textsf{Focal} Development Team}",
title = "\textsf{Focal}, version~0.3.1",
organization = "\textsf{Cnam}, \textsf{Inria}, and \textsf{LIP6}",
month = may,
year = 2005,
note = "\url{http://focal.inria.fr/}"
}
- David Delahaye, Mathieu Jaume, and Virgile Prevosto. Coq: un outil pour
l'enseignement. Technique et Science Informatiques (TSI),
24(9):1139—1160, 2005.
PDF
@article{Coq-Ens,
author = "Delahaye, David and Jaume, Mathieu and Prevosto, Virgile",
title = "{\textsf{Coq}: un outil pour l'enseignement}",
journal = "Technique et Science Informatiques (TSI)",
volume = 24,
number = 9,
pages = "1139--1160",
year = 2005
}
Cited by
2002
- David Delahaye. Free-Style Theorem Proving. In Victor Carreño, César Muñoz,
and Sofiène Tashar, editors, Theorem Proving in Higher Order Logics
(TPHOLs), volume 2410 of Lecture Notes in Computer Science (LNCS),
pages 164—181, Hampton (VA, USA), August 2002. Springer.
The original publication is available at www.springerlink.com.
PDF
@inproceedings{Lpdt,
author = "Delahaye, David",
title = "{Free-Style Theorem Proving}",
booktitle = "Theorem Proving in Higher Order Logics (TPHOLs)",
editor = "Carreño, Victor and Muñoz, César and Tashar, Sofiène",
publisher = "Springer",
series = "Lecture Notes in Computer Science (LNCS)",
address = "Hampton (VA, USA)",
volume = 2410,
pages = "164--181",
month = aug,
year = 2002
}
Cited by - David Delahaye. A Proof Dedicated Meta-Language. In Frank Pfenning, editor,
Logical Frameworks and Meta-Languages (LFM), as part of the Federated Logic
Conference (FLoC), volume 70(2) of Electronic Notes in Theoretical
Computer Science (ENTCS), pages 96—109, Copenhagen (Denmark), July
2002. Elsevier.
PDF
@inproceedings{Ltac2,
author = "Delahaye, David",
title = "{A Proof Dedicated Meta-Language}",
booktitle = "Logical Frameworks and Meta-Languages (LFM)",
editor = "Pfenning, Frank",
publisher = "Elsevier",
series = "Electronic Notes in Theoretical Computer Science (ENTCS)",
address = "Copenhagen (Denmark)",
volume = "70(2)",
pages = "96--109",
month = "July",
year = 2002
}
Cited by
2001
- David 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. PhD thesis, Université Pierre et Marie Curie (Paris 6),
December 2001.
PDF
@phdthesis{PhD-Thesis,
author = "Delahaye, David",
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 \textsf{Coq}",
school = "Université Pierre et Marie~Curie (Paris~6)",
month = dec,
year = 2001
}
- David Delahaye and Micaela Mayero. Field: une procédure de décision pour les
nombres réels en Coq. In Pierre Castéran, editor, Journées Francophones des
Langages Applicatifs (JFLA), pages 33—48, Pontarlier (France), January
2001. Inria.
The original publication is available at jfla.inria.fr.
PDF
@inproceedings{Field,
author = "Delahaye, David and Mayero, Micaela",
title = "{\texttt{Field}: une procédure de décision pour les nombres réels en \textsf{Coq}}",
booktitle = "Journées Francophones des Langages Applicatifs (JFLA)",
editor = "Castéran, Pierre",
publisher = "\textsf{Inria}",
address = "Pontarlier (France)",
pages = "33--48",
month = jan,
year = 2001
}
Cited by
2000
- David Delahaye. A Tactic Language for the System Coq. In Michel Parigot and
Andrei Voronkov, editors, Logic for Programming and Automated Reasoning
(LPAR), volume 1955 of Lecture Notes in Computer Science (LNCS)/Lecture
Notes in Artificial Intelligence (LNAI), pages 85—95, Reunion Island
(France), November 2000. Springer.
The original publication is available at www.springerlink.com.
PDF
@inproceedings{Ltac,
author = "Delahaye, David",
title = "{A Tactic Language for the System \textsf{Coq}}",
booktitle = "Logic for Programming and Automated Reasoning (LPAR)",
editor = "Parigot, Michel and Voronkov, Andrei",
publisher = "Springer",
series = "Lecture Notes in Computer Science (LNCS)/Lecture Notes in Artificial Intelligence (LNAI)",
address = "Reunion Island (France)",
volume = 1955,
pages = "85--95",
month = nov,
year = 2000
}
Cited by
1999
- David Delahaye. Information Retrieval in a Coq Proof Library using Type
Isomorphisms. In Thierry Coquand, Peter Dybjer, Bengt Nordström, and Jan Smith,
editors, TYPES, volume 1956 of Lecture Notes in Computer Science
(LNCS), pages 131—147, Lökeberg (Sweden), June 1999. Springer.
The original publication is available at www.springerlink.com.
PDF
@inproceedings{SearchIsos,
author = "Delahaye, David",
title = "{Information Retrieval in a \textsf{Coq} Proof Library using Type Isomorphisms}",
booktitle = "Types for Proofs and Programs (TYPES)",
editor = "Coquand, Thierry and Dybjer, Peter and Nordström, Bengt and Smith, Jan",
publisher = "Springer",
series = "Lecture Notes in Computer Science (LNCS)",
address = "Lökeberg (Sweden)",
volume = 1956,
pages = "131--147",
month = jun,
year = 1999
}
Cited by