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

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!