Curriculum Vitæ
Version Pdf.
Matthieu Sozeau
Adresse:
201 rue Saint Maur
75010 Paris
France
Téléphone:
(+33) 6 88 36 74 27
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, preuve automatique
  • Programmation fonctionnelle et générique
  • Applications de la théorie des catégories à l'informatique
Projets

  • ANR Typex - White program (2012-2014, 36m). "Intégration des approches langage, logique et orientée données pour un traitement XML certifié, dirigé par les types." PPS (G. Castagna, coord.), INRIA Paris (pi.r2) and Grenoble (WAM), LRI. Task leader.
  • ANR Paral-ITP (2012-2014, 36m). Parallelization of interactive theorem provers. Univ. Paris-Sud / LRI (B. Wolff, coord.), INRIA Rocquencourt (H. Herbelin, PPS), INRIA Saclay (B. Barras).
Livres

Revues internationales avec comité de lecture

Conférences internationales avec comité de sélection

  • Universe Polymorphism in Coq in ITP'14. Matthieu Sozeau & Nicolas Tabareau. Vienna, Austria, 2014 - To appear.
  • Extending Type Theory with Forcing in Proceedings of LICS'12. Jaber, Guilhem, Tabareau, Nicolas & Sozeau, Matthieu. Dubrovnik, Croatie, June 2012.
  • Equations: A Dependent Pattern-Matching Compiler in First International Conference on Interactive Theorem Proving. Matthieu Sozeau. Springer, July 2010.
  • First-Class Type Classes in TPHOLs. Matthieu Sozeau & Nicolas Oury. Otmane Ait Mohamed, César Muñoz and Sofiène Tahar (Eds). Volume 5170 of LNCS. Springer, August 2008, pp.278-293.
    (18/40)
  • Program-ing Finger Trees in Coq in ICFP'07. Matthieu Sozeau. Freiburg, Germany: ACM Press, 2007, pp.13-24.
    (26/103)
  • Subset Coercions in Coq in TYPES'06. Matthieu Sozeau. Thorsten Altenkirch and Conor McBride (Eds). Volume 4502 of Lecture Notes in Computer Science. Springer, 2007, pp.237-252.
    (17/29)
Groupes de travail internationaux avec comité de sélection

Conférences nationales avec comité de sélection

Mémoires

Manuels, Tutoriels

Présentations invitées et séminaires extérieurs

Présentations en conférences et séminaires locaux

Emplois, stages

  • Depuis Octobre 2010:
    INRIA Paris, pi.r2 team -
    Chargé de Recherche.
  • Mars 2009 - Septembre 2010:
    Harvard University -
    Postdoc.
  • Septembre à Décembre 2008:
    Université Paris XI -
    Poste d'ingénieur-chercheur du CNRS sur le projet SCALP.
  • 2005-2008:
    Université Paris XI -
    Thèse de doctorat sur une bourse MENRT.
  • 2005-2008:
    Université Paris XI -
    Monitorat à l'UFR de Sciences.
  • Mars à Septembre 2005:
    Université Paris XI -
    Stage de Master sur les coercions de sous-ensembles dans Coq.
    Sous la direction de
    Christine Paulin-Mohring
    .
  • Juillet et août 2004:
    Laboratoire d'informatique de l'ENS -
    Stage sur l'optimisation du filtrage dans CDuce.
    Sous la direction de
    Giuseppe Castagna
    .
  • Avril à juin 2004:
    Laboratoire de recherche en informatique de Paris XI -
    TER-Stage sur la triangulation de graphes.
    Sous la direction de
    Pascal Berthomé
    .
  • Été 2003:
    Laboratoire de physique des solides de Paris XI -
    Optimisation d'une application de traitement vidéo temps-réel.
    Sous la direction de
    Pierre Garoche
    .
  • Été 2002:
    Thalès -
    Mise à jour d'une application de gestion de produits.
  • Septembre 2000:
    Manpower -
    Manutentionnaire.
Scolarité

  • 2009-10:
    Université d'Harvard
    -
    Post-doctorat en Informatique.
    Avec Greg Morrisett.
  • 2005-08:
    Université Paris XI
    -
    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
    -
    Maitrise d'Informatique.
    Mention bien.
  • 2002-03:
    Université Paris XI
    -
    Licence d'Informatique.
    Mention bien.
  • 2000-02:
    IUT d'Orsay (Paris XI)
    -
    DUT d'Informatique.
    Mention bien.
Expériences en développement

  • Contributeur majeur à l'outil Coq écrit en OCaml
  • Sites utilisant 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 programmation OCaml, Coq, Haskell, C, assembleurs, C++, LISP, Java, Ruby, Python
  • Langages W3C: XML, XHTML, XPath, XSLT, CSS
  • 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

  • Yaxi, une librairie XML/XPath/XSLT pour OCaml
  • Hamilcar, serveur d'application XML pour OCaml
  • Ancien développeur Gentoo Linux et XMMS
Valid XHTML 1.1! Valid CSS!