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

  • Type theory, dependently-typed programming and constructive logic
  • Interactive proof assistants: coordinator of the Coq development team
  • Links between category theory and type theory
Projects and Grants

  • ERC Starting Grant CoqHoTT led by Nicolas Tabareau (Inria Rennes, École des Mines de Nantes), 2015-2020. Collaborator.

International Conferences

International Workshops

National Conferences


Research Reports


Manuals and Tutorials

Invited Talks and Seminars

Community service

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!