Matthieu Sozeau :: Curriculum Vitae

Curriculum Vitae

PostScript, pdf versions.

Matthieu Sozeau

Adress:

7, rue d'Estienne d'Orves
94230 Cachan
France

Phone:

06 81 20 38 92

Email:

Matthieu.Sozeau@lri.fr

Website:

http://www.lri.fr/~sozeau

Research interests

Type theory and constructive logic
Formal methods, particularly construction and proof of dependently-typed programs
Functional and generic programming

Education

2005-(08):
Paris XI University - Orsay
-
PhD in Computer Science.
(Predicted) title: An environment for programming with dependent types.
2004-05:
Paris VII University - Denis Diderot
-
Master of research in Computer Science.
Grade A.
2003-04:
Paris XI University
-
"Maitrise" of Computer Science.
Grade B.
2002-03:
Paris XI University
-
Licence in Computer Science.
Grade B.
2000-02:
Orsay's Institute of Technology
-
University Diploma of Technology in Computer Science.
Grade B.
1997-00:
Lycée de la Vallée de Chevreuse
-
Scientific bachelor, mathematics speciality.
Grade C.

Publications

First-Class Type Classes in Theorem Proving in Higher Order Logics, 21th International Conference. Matthieu Sozeau and Nicolas Oury. Otmane Ait Mohamed, César Muñoz and Sofiène Tahar (Eds). Volume 5170 of Lecture Notes in Computer Science. Springer, August 2008, pp.278-293.
DOI
slides
Program-ing Finger Trees in Coq in ICFP'07: Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming. Matthieu Sozeau. ACM Press, Freiburg, Germany, 2007, pp.13--24.
© ACM, 2007. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ICFP'07, http://doi.acm.org/10.1145/1291151.1291156
DOI
slides
Subset Coercions in Coq in TYPES'06. Matthieu Sozeau. Volume 4502 of Lecture Notes in Computer Science. Springer, 2007, pp.237--252.
© Springer
DOI
slides
Coercion par prédicats en Coq. Matthieu Sozeau, Master's Thesis,Université Paris VII, LRI, Orsay, 2005 - In french.

Reference Manual Chapters

`Type Classes' in Coq 8.2 Reference Manual. Matthieu Sozeau. INRIA TypiCal, Available at http://coq.inria.fr/V8.2beta4/doc/refman/html/Reference-Manual024.html, 2008.
`User defined equalities and relations' in Coq 8.2 Reference Manual. Matthieu Sozeau. INRIA TypiCal, Available at http://coq.inria.fr/V8.2beta4/doc/refman/html/Reference-Manual029.html, 2008.
`Program' in Coq 8.2 Reference Manual. Matthieu Sozeau. INRIA TypiCal, Available at http://coq.inria.fr/V8.2beta4/doc/refman/html/Reference-Manual027.html, 2008.

Talks

First-Class Type Classes. Matthieu Sozeau, Talk given at the Gallium seminar, Rocquencourt, 3rd November 2008.
First-Class Type Classes. Matthieu Sozeau, Talk given at TPHOLs'08, Montréal, Canada, 20th August 2008.
First-Class Type Classes, in Coq. Matthieu Sozeau, Talk given at the ProVal workgroup, Orsay, 3rd March 2008.
Dependent Finger Trees. Matthieu Sozeau, Talk given at DTP'08, Nottingham, UK, 18--20 February 2008.
Program-ing in Coq. Matthieu Sozeau, Talk given at Harvard, Cambridge, MA, 23th january 2008.
Program-ing in Coq. Matthieu Sozeau, Talk given at Portland State University, Portland, OR, 16th january 2008.
Program-ing Finger Trees in Coq. Matthieu Sozeau, Talk given at ICFP'07, Freiburg, Germany, 1--3 October 2007.
A journey with Russell: Programming Dependent Finger Trees in Coq. Matthieu Sozeau, Talk given at TYPES'07, Cividale Del Friuli, Italy, 2-5 May 2007.
Program-ing in Coq. Matthieu Sozeau, Talk given at the Gallium seminar, Rocquencourt, 16th march 2007.
Program-ing in Coq. Matthieu Sozeau, Talk given at the ProVal seminar, Orsay, 9th march 2007.
Subset Coercions in Coq. Matthieu Sozeau, Talk given at TYPES'06, University of Nottingham, UK, 19-21 april 2006.

Jobs and internships

2005-2008:
Paris XI University - Orsay -
Teaching assistant position in Computer Science.
March to September 2005:
Paris XI University - Orsay -
Master internship on the development of an environment for programming with dependent types.
Under the direction of
Christine Paulin-Mohring
.
July / August 2004:
Computer Science Laboratory of ENS Ulm -
Internship on optimisation of pattern-matching in CDuce.
Under the direction of
Giuseppe Castagna
.
April to June 2004:
Laboratoire de recherche en informatique, Paris XI University -
Internship on graph triangulation.
Under the direction of
Pascal Berthomé
.
Summer 2003:
Laboratoire de physique des solides, Paris XI University -
Optimisation of a real-time video process.
Under the direction of
Pierre Garoche
.
Summer 2002:
Thalès -
Update and maintenance of a product managment software.
September 2000:
Manpower -
Interim work.

Development experience

Technical Knowledge

W3C Markup languages
Programming languages: O'Caml, Coq, Haskell, C, asm x86, C++, Java, Python, Ruby
Program certification and theorem proving in the Coq proof-assistant
Administration under GNU/Linux of Apache, Samba, Squid, CUPS, qmail, courrier, iptables, nfs and nis

Open Source software

Hobbies