Christine Paulin-Mohring    Professor Université Paris-Sud Team-Project PROVAL, INRIA Saclay - Île-de-France Bat N, Bureau 117 Parc Orsay Université, Zac des Vignes 4, rue Jacques Monod, 91893 Orsay cedex, France & LRI, UMR 86223 CNRS Université Paris Sud, 91405 ORSAY Cedex, France tel (+33) (0)1 72 92 59 05 fax (+33) (0)1 74 85 42 29 mail Christine.Paulin@lri.fr

Research

• Scientific leader of the INRIA research project-team ProVal (common PCRI project: université Paris Sud, CNRS, École Polytechnique and INRIA Saclay - Île-de-France)
• Head of the team Démons
• Editorial board: Journal of Formalized Reasoning
• Member of Program committees:
  • 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)
  • TPHOLs’08 : 21st International Conference on Theorem Proving in Higher Order Logics, 18-21 August 2008, Montréal, Canada
  • MPC ’08: Mathematics of Program Construction, 15-18 July 2008, CIRM, Luminy, France (chair)
  • TPHOLs’07 20th International Conference on Theorem Proving in Higher Order Logics, 11-13 September 2007, Kaiserslautern, Germany
  • WoLLIC’2007 14th Workshop on Logic, Language, Information and Computation July 2-5, 2007, Rio de Janeiro, Brazil
  • IJCAR : International Joint Conference on Automated Reasoning August 16-21, 2006, Seattle (part of FLOC’06)
  • JFLA’2006 Journées Francophones des Langages Applicatifs 28-31 janvier 2006, Pauillac, France
• Past events
  • 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
  • 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
  • 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 - new version 5 - nov 2010 (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)

Teaching

• 2004- Master Parisien de Recherche en Informatique
  • Assistants de Preuve (M2 course 2010-2011)
• 2005- Director of the École Doctorale d’Informatique de l’Université Paris Sud.
• 2008- Master informatique M1 (maîtrise)
  • Compilation (Cours-TD-Projet)
• 2009- Licence Sciences Technologie Santé, S4 -
  • Mathématiques pour l’Informatique (2010-11) (Cours-TD-Projet)
  • Langages et Génie Logiciel (2009-10) (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.