 |
|
Short biography
Research
- (until 2015) Member of the INRIA research project-team Toccata (formerly ProVal) (common project: Université Paris Sud, CNRS and INRIA Saclay - Île-de-France)
- (until 2015) Scientific coordinator of the DigiCosme Labex
- Editorial board: Journal of Formalized Reasoning
- Member of Program committees :
- ITP 2022 Thirteenth Conference on Interactive Theorem Proving Haifa, Israel, 2022
- LICS 2016 Thirty First Annual ACM/IEEE Symposium on Logic in Computer Science. 5-8 July 2016. New York City. USA.
- LPAR-20 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning. 24-November 2015. Suva. Fiji.
- Types 2015 21st International Conference on Types for Proofs and Programs. 18-21 May 2015. Tallin. Estonia.
- MPC 2015 Mathematics of Program Construction. 29 June - 1 July 2015. Königswinter, Germany.
- CPP 2015 Certified Programs and Proofs. 13-14 January, 2015. Mumbai, India (colocated with POPL 2015)
- ITP 2014 Interactive Theorem Proving. 14-17 July, 2014. Vienna, Austria.
- Coq workshop, Vienna, Austria, July 18, 2014, as part of Vienna Summer of Logic.
- ITP 2013 Interactive Theorem Proving. 22-26 July, 2013. Rennes, France. (member of the organising committee)
- ITP 2012 Interactive Theorem Proving. 13-16 August, 2012. Princeton, New Jersey.
- PLPV 2011 The Fifth ACM SIGPLAN Workshop on Programming Languages meets Program Verification. 29th January, 2011. Austin, Texas (Affiliated with POPL 2011)
- ITP 2011 Interactive Theorem Proving. 22-25 August 2011. Nijmegen, The Netherlands
- Third Coq workshop, Nijmegen, the Netherlands, August 26th, 2011, as part of ITP 2011.
- MPC ’10: Mathematics of Program Construction, 21-23 June 2010, Manoir St-Castin Québec, Canada
- The 2nd Coq Workshop, Edinburgh, Scotland. 9 July, 2010 (A satellite workshop of ITP 2010)
- See all program committees
- Past events
- Co-organizer with Zhong Shao of the workshop on Certification of high-level and low-level programs, July 7-11, 2014, as part of the IHP thematic trimester Semantics of proofs and certified mathematics April-July, 2014. Paris, France.
- Organisation of the
Mathematics of Program Construction (MPC ’08) conference.
CIRM, Luminy, France, 15-18 July 2008. - Colloquium in honor of Gérard Huet June 22th and 23th, 2007, École Normale Supérieure, Paris.
- Summerschools
-
8th LASER Summer School on Software Engineering (LASER 2011) Tools for Practical Software Verification
September 4-10, 2011 - Elba Island, Italy
Documents for the course Post summerschool paper: Introduction to the Coq proof-assistant for practical software verification - Types Summer School, August 19-31th, 2007 Bertinoro - Italy slides
- Types Summer School 2005 Slides : advi, ps, ps (4 per page)
- Summer School on Foundations of Security (2003)
Course notes on inductive definitions
-
8th LASER Summer School on Software Engineering (LASER 2011) Tools for Practical Software Verification
September 4-10, 2011 - Elba Island, Italy
- Research projects
- Semantics of a skeleton language for parallel programs
- Denotational semantics for Kahn Networks
- Proofs of randomized algorithms
ANR Project SCALP (2007-2011)
- Description of the Coq library - version 8 (including
a library for positive real numbers) - May 2013 - runs with Coq V8.4
(pdf version)
Coq Source files of the library - Coq library - version 7 (including
a library for positive real numbers) - Feb 2012 - runs with Coq V8.3
(pdf version)
Coq Source files of the library - Coq library - version 6 - Dec 2011
(pdf version)
Coq Source files of the library
- Description of the Coq library - version 8 (including
a library for positive real numbers) - May 2013 - runs with Coq V8.4
(pdf version)
- Proofs of Java programs
ACI security project: GECCOO (2003-2006)
- Site leader and member of the steering committee
of the europeean Coordination Action
TYPES
- We organised the international workshop TYPES’2004, Jouy-en Josas, 15-18 décembre 2004
- Working groups Maths in Coq
- Report 2006-PDF
- Report 2005(PDF)
Distinctions
- Doctor Honoris Causa, University of Gothenburg
- Prix Michel Monpetit (2015), Academy of Science, France
- Member of the Academia Europaea, section informatics (elected in 2014)
- ACM software system award (2013) for the Coq Proof Assistant
- Member of the Coq development team which receives in 2013 the ACM SIGPLAN Programming Languages Software Award
Administration
- 2016-2021 Dean of the Faculty of Science, Université Paris-Sud/Paris-Saclay
- 2014-2016 Member of the Scientific Council of Telecom SudParis
- 2012-2014 In charge of the “Collège des Ecoles Doctorales” Univ. Paris-Sud
- 2012-2014 Head of the computer science department at Univ. Paris-Sud
- 2011 Deputy director, LRI
- 2010-2013 Member of the Scientific Council of ENS Cachan
- 2007-2010 Deputy scientific director, INRIA Saclay–Île-de-France
- 2005-2010 Member of the national evaluation board of INRIA
Teaching
- 2015-17 M2 Master Informatique Parcours FIIL/Science du Logiciel Preuves Interactives et Applications (avec Burkhart Wolff)
- 2013-15 Agregation - option informatique - logique
- 2009- Licence Sciences Technologie Santé
- S4 - Mathématiques pour l’Informatique 2 (2014-16) (Cours-TD-Projet)
- S4 - Mathématiques pour l’Informatique (2010-14) (Cours-TD-Projet)
- S5 - Eléments de logique pour l’informatique (2012-) (Cours-TD)
- S4 - Langages et Génie Logiciel (2009-10) (Cours-TD-Projet)
- 2004-2011
Master Parisien de Recherche en Informatique
- Assistants de Preuve (M2 course 2010-2011)
- 2005-2012 Director of the École Doctorale d’Informatique de l’Université Paris Sud.
- 2008-2012 Master informatique M1 (maîtrise)
- Compilation (Cours-TD-Projet)
- 2004-2005 In charge of master mention informatique
- 1998-2005 In charge of licence and maîtrise in computer science
- Deug 2004-2005
- Compétences Complémentaires en Informatique (CCI) 2004-2005
- DEA Sémantique, Preuves et Langages 2003-2004
Publications
- Publications
- Coq formation 25-27 février 2002
Software developments
- Proof assistant Coq
- Krakatoa Proof of Java programs annotated with JML specifications.
This document was translated from LATEX by HEVEA.