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:
MPC ’10: Mathematics of Program Construction, 21-23 June 2010, Manoir St-Castin Québec, Canada
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
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 4 - 2009
(
HTML 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 2008-2009)
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 -
Langages et Génie Logiciel
(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
A
T
E
X by
H
E
V
E
A
.