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
  • 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

  • A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading in ACM SIGPLAN International Conference on Functional Programming 2015. Beta Ziliani & Matthieu Sozeau. , 2015.
  • Universe Polymorphism in Coq in Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. Matthieu Sozeau & Nicolas Tabareau. , 2014, pp.499-514.
  • 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.
  • Program-ing Finger Trees in Coq in ICFP'07. Matthieu Sozeau. Freiburg, Germany: ACM Press, 2007, pp.13-24.
  • 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.
International Workshops

National Conferences


Manuals and Tutorials

Invited Talks and Seminars

Conference Talks and Local 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!