Matthieu Sozeau :: Curriculum Vitæ

Curriculum Vitæ

Versions PostScript, pdf.

Matthieu Sozeau

Adresse:

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

Téléphone:

06 81 20 38 92

Email:

mattam@mattam.org

Site web

http://mattam.org

Domaines de recherche

Théorie des types et logique constructive
Méthodes formelles, construction et preuve de programmes utilisant les types dépendants
Programmation fonctionnelle et générique

Scolarité

2005-08:
Université Paris XI - Orsay
-
Thèse de Doctorat en Informatique.
Mention très honorable.
2004-05:
Université Paris VII - Denis Diderot
-
Master 2 Recherche en Informatique (MPRI).
Mention très bien.
2003-04:
Université Paris XI - Orsay
-
Maitrise d'Informatique.
Mention bien.
2002-03:
Université Paris XI - Orsay
-
Licence d'Informatique.
Mention bien.
2000-02:
IUT d'Orsay (Paris XI)
-
DUT d'Informatique.
Mention bien.
1997-00:
Lycée de la Vallée de Chevreuse
-
Bac Scientifique spécialité mathématiques.
Mention assez bien.

Publications

Un environnement pour la programmation avec types dépendants. Matthieu Sozeau, PhD Thesis,Université Paris 11, December 2008.
slides
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.

Chapitres de manuel de référence

`Type Classes' in Coq 8.2 Reference Manual. Matthieu Sozeau. INRIA TypiCal, 2008.
`User defined equalities and relations' in Coq 8.2 Reference Manual. Matthieu Sozeau. INRIA TypiCal, 2008.
`Program' in Coq 8.2 Reference Manual. Matthieu Sozeau. INRIA TypiCal, 2008.

Présentations

An Environment for Programming with Dependent Types. Matthieu Sozeau, Thesis Defense,Paris 11 University, 8th December 2008.
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.

Emplois, stages

Expérience en développement

Contributeur majeur à l'outil Coq écrit en OCaml
Sites et serveurs web utitlisants les CGI, LAMP, XML/XSLT/XSP coté serveur, applets ou HTML/JavaScript coté client
C, C++ et programmation assembleur, optimisation pour x86
Programmation OpenGL en C et OCaml

Connaissances Techniques en Informatique

Langages de balisages XML, XHTML, HTML
Langages de programmation OCaml, Coq, C, assembleur x86, C++, haskell, LISP, Java, Ruby, Python
Programmation et démonstration dans l'assistant de preuve Coq
Administration sous GNU/Linux de Apache(/Jakarta), Samba, Squid, CUPS, qmail, courrier, routage, NFS et NIS

Projets libres

Hobbies