introduction

Christine Paulin-Mohring

Professor Université Paris-Sud, Team VALS & Inria project Toccata

LRI, UMR 8623 CNRS, Université Paris Sud & INRIA Saclay - Île-de-France

Postal address : Bat 650 (Ada Lovelace), Univ. Paris Sud, 91405 Orsay Cedex, France

Location : office 74, Bat 650 South, Rue Noetzlin, 91190 Gif sur Yvette, France

tel	(+33) (0)1 69 15 64 39
fax	(+33) (0)1 74 85 42 29
mail	Christine.Paulin@lri.fr

Short biography

Research

Member of the INRIA research project-team Toccata (formerly ProVal) (common project: Université Paris Sud, CNRS and INRIA Saclay - Île-de-France)
Scientific coordinator of the DigiCosme Labex
Editorial board: Journal of Formalized Reasoning
Member of Program committees :
- 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
Research projects
- Semantics of a skeleton language for parallel programs
- Denotational semantics for Kahn Networks
  - Description of the Coq library - Version July 2007 (HTML version)
    Coq Source files of the library
- 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
- 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

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

2014- 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- M2 Master Informatique Parcours FIIL/Science du Logiciel Preuves Interactives et Applications (avec Burkhart Wolff)
2013- Agregation - option informatique - logique
2009- Licence Sciences Technologie Santé
- S4 - Mathématiques pour l’Informatique 2 (2014-) (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
- S3 MIAS Approche fonctionnelle (Cours-TD)
Compétences Complémentaires en Informatique (CCI) 2004-2005
- Principes des Langages de Programmation (Cours)
DEA Sémantique, Preuves et Langages 2003-2004
- Calcul des Constructions Inductives (Cours)

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 L^AT_EX by H^EV^EA.