Curriculum Vitæ
Pdf version.
Matthieu Sozeau
59 rue de la Chine
75020 Paris
(+33) 6 88 36 74 27
Research interests

  • Type theory and constructive logic, lead developer of the Coq proof-assistant
  • Formal methods, particularly construction and proof of dependently-typed programs
  • Functional and generic programming
  • Applications of Category Theory to Computer Science
Projects and Grants

  • ERC Starting Grant CoqHoTT led by Nicolas Tabareau (Inria Rennes, École des Mines de Nantes), 2015-2020. Collaborator.
  • 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).
Community service


International Conferences

International Workshops

National Conferences


Research Reports


Manuals and Tutorials

Invited Talks and Seminars

Jobs and internships

  • Since October 2010:
    INRIA Paris, pi.r2 team -
    Junior Researcher.
  • March 2009 - September 2010:
    Harvard University -
    Postdoctoral Fellow.
  • September to December 2008:
    Paris XI University -
    Temporary researcher at CNRS.
  • 2005-2008:
    Paris XI University -
    PhD Thesis funded by the french government.
  • 2005-2008:
    Paris XI University -
    Teaching assistant position in Computer Science.
  • March to September 2005:
    Paris XI University -
    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.

  • 2009-10:
    Harvard University
    Postdoctoral studies in the Ynot group.
    Working with Greg Morrisett and his team on Coq and Ynot.
  • 2005-08:
    Paris XI University
    PhD in Computer Science.
    With honors.
  • 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.
Development experience

  • Major contributor to the Coq project written in OCaml
  • Web development using CGIs, LAMP, XML/XSLT/XSP's, Java applets, Javascript
  • C, C++ and assembly programming, optimization for x86
  • OpenGL programming in C and OCaml
Technical Knowledge

  • Programming languages: OCaml, Coq, Haskell, C, asm x86, C++, Java, Python, Ruby
  • W3C Markup languages: XML, XHTML, XPath, XSLT, CSS
  • 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

  • Yaxi, an XML/XPath/XSLT library for OCaml
  • Hamilcar, an XML application server in OCaml
  • Former developer for Gentoo Linux (OCaml, Coq maintainer), XMMS (ALSA plugin), Dia (UML, XSLT export), Apache Cocoon (i18n, CVS repository viewer).
  • Various toy projects: webapp server in Ruby, distributed file index in Python, networked coinche (french card game) in OCaml, Bomberman in C++/OpenGL, Genealogy engine in Boost/C++.
Valid XHTML 1.1! Valid CSS!