Matthieu Sozeau :: Curriculum Vitæ

Curriculum Vitæ

Pdf version.

Matthieu Sozeau

Adress:

217 rue la Fayette
75010 Paris
France

Phone:

(+33) 6 88 36 74 27

Email:

mattam@mattam.org

Website:

http://mattam.org

Research interests

Type theory and constructive logic
Formal methods, particularly construction and proof of dependently-typed programs
Functional and generic programming

Journals

Partiality and Recursion in Interactive Theorem Provers - An Overview. Ana Bove and Alexander Krauss and Matthieu Sozeau To appear in MSCS, January 2011.
A New Look at Generalized Rewriting in Type Theory. Matthieu Sozeau Journal of Formalized Reasoning 2 (1), December 2009, pp.41-62.

International Conferences

Extending Type Theory with Forcing in Proceedings of LICS'12. Jaber, Guilhem and Tabareau, Nicolas and 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.
slides
(33/74)
First-Class Type Classes in Theorem Proving in Higher Order Logics, 21th International Conference. Matthieu Sozeau and Nicolas Oury. Otmane Ait Mohamed, César Muñoz and Sofiène Tahar (Eds). Volume 5170 of Lecture Notes in Computer Science. Springer, August 2008, pp.278-293.
© Springer
DOI
slides
(18/40)
Program-ing Finger Trees in Coq in ICFP'07: Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming. Matthieu Sozeau. Freiburg, Germany: ACM Press, 2007, pp.13--24.
© ACM, 2007. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ICFP'07, http://doi.acm.org/10.1145/1291151.1291156
DOI
slides
(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.
© Springer
DOI
slides
(17/29)

International Workshops

A New Look at Generalized Rewriting in Type Theory. Matthieu Sozeau 1st Coq Workshop proceedings, August 2009.
slides

National Conferences

Classes de types de première classe in Journées Nationales du GDR GPL. Matthieu Sozeau and Nicolas Oury. Toulouse, France, January 2009.
slides

Theses

Un environnement pour la programmation avec types dépendants. Matthieu Sozeau, PhD Thesis, Université Paris 11, Orsay, France, December 2008.
slides
Coercion par prédicats en Coq. Matthieu Sozeau, Master's Thesis, Université Paris VII, LRI, Orsay, 2005.

Manuals and Tutorials

A Gentle Introduction to Type Classes and Rewriting in Coq. Pierre Castéran and Matthieu Sozeau, Misc, May 2012.
`Type Classes' in Coq Reference Manual. Matthieu Sozeau. INRIA TypiCal, 2008--2012.
`User defined equalities and relations' in Coq Reference Manual. Matthieu Sozeau. INRIA TypiCal, 2008--2012.
`Program' in Coq Reference Manual. Matthieu Sozeau. INRIA TypiCal, 2008--2012.

Projects and Grants

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 leadear.
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

Co-organizer and PC member of DTP'11
PC member: TLDI'10, ICFP'10, MSFP'12, PLPV'12
External reviews: Journal of Functional Programming, Fundamenta Informaticae, Logical Methods in Computer Science, Mathematical Structures in Computer Science, TPHOLs'08, FLOPS'08, TPHOLs'09, PPDP'09, TYPES'09, LICS'10, ITP'10, ICFP'11, CPP'11, TLCA'11, POPL'12

Invited Talks and Seminars

Coq with Classes. Matthieu Sozeau, Lecture at the "Advanced Martial Arts in Coq" course at University of Pennsylvania, October 2012.
Coq with Classes. Matthieu Sozeau, Talk given at the IAS seminar in Princeton, NJ, October 2012.
Equations: A Dependent Pattern-Matching Suite. Matthieu Sozeau, Talk given at the Institute of Cybernetics, Tallinn, Estonia, May 2012.
Coq with Classes. Matthieu Sozeau, Lecture notes for a course given at JFLA'12 in Carnac, France, February 2012.
Coq with Classes. Matthieu Sozeau, Talk given at the PLAS seminar in Canterbury - UK, November 2011.
Coq with Classes. Matthieu Sozeau, Talk given at the IMDEA seminar in Madrid - Spain, October 2011.
Coq with Classes. Matthieu Sozeau, Talk given at the PPS days in Trouville - France, September 2011.
Equations: A Dependent Pattern-Matching Suite. Matthieu Sozeau, Talk given at the DTP meeting in Shonan - Japan, September 2011.
Equations: A Dependent Pattern-Matching Compiler. Matthieu Sozeau, Talk given at University of Chalmers - Gothenburg, January 2011.
Equations: A Dependent Pattern-Matching Compiler. Matthieu Sozeau, Talk given at the University of Pennsylvania PLClub, September 2010.
Elaborations in Type Theory. Matthieu Sozeau, Invited Talk at DTP'10 - Edinburgh, UK, July 2010.
Equations: A Dependent Pattern-Matching Compiler. Matthieu Sozeau, Talk given at PPS - Université Paris 7, January 2010.
Programming with Dependent Types in Coq. Matthieu Sozeau, PPS Seminar, Paris, France, 26th February 2009.
An Environment for Proving and Programming. Matthieu Sozeau, LIFO Seminar, Orléans, France, 26th January 2009.
An Environment for Programming with Dependent Types. Matthieu Sozeau, ICIS Seminar, Nijmegen, Netherlands, 20th January 2009.
First-Class Type Classes. Matthieu Sozeau, Talk given at the Gallium seminar, Rocquencourt, 3rd November 2008.
Program-ing in Coq. Matthieu Sozeau, Talk given at the Foundations of Programming seminar, Nottingham, UK, 15th February 2008.
Program-ing in Coq. Matthieu Sozeau, Talk given at Harvard, Cambridge, MA, 23th january 2008.
Program-ing in Coq. Matthieu Sozeau, Talk given at Portland State University, Portland, OR, 16th january 2008.
Program-ing in Coq. Matthieu Sozeau, Talk given at the Gallium seminar, Rocquencourt, 16th march 2007.

Conference Talks and Local Seminars

Coq with Classes. Matthieu Sozeau, Tutorial given at the IAS, Princeton, NJ, December 10th 2012.
Universe Polymorphism and Inference in Coq. Matthieu Sozeau, Talk given at the Institute for Advanced Study, Princeton, NJ, December 5th 2012.
Equations: A Dependent Pattern-Matching Compiler. Matthieu Sozeau, Talk given at TYPES'10, Warsaw, Poland, October 2010.
Equations: A Dependent Pattern-Matching Compiler. Matthieu Sozeau, Talk given at ITP'10, Edinburgh, UK, July 2010.
A New Look at Generalized Rewriting in Type Theory. Matthieu Sozeau, Talk given at the First Coq Workshop, Munich, Germany, August 2009.
A New Look at Generalized Rewriting in Type Theory. Matthieu Sozeau, TYPES'09, Aussois, France, May 2009.
First-Class Type Classes. Matthieu Sozeau, Talk given at the GDR GPL, ENSEEIHT - Toulouse, 30th January 2009.
An Environment for Programming with Dependent Types. Matthieu Sozeau, Thesis Defense, Paris 11 University, Orsay, France, 8th December 2008.
First-Class Type Classes. Matthieu Sozeau, Talk given at TPHOLs'08, Montréal, Canada, 20th August 2008.
First-Class Type Classes, in Coq. Matthieu Sozeau, Talk given at the ProVal workgroup, Orsay, 3rd March 2008.
Dependent Finger Trees. Matthieu Sozeau, Talk given at DTP'08, Nottingham, UK, 18--20 February 2008.
Program-ing Finger Trees in Coq. Matthieu Sozeau, Talk given at ICFP'07, Freiburg, Germany, 1--3 October 2007.
A journey with Russell: Programming Dependent Finger Trees in Coq. Matthieu Sozeau, Talk given at TYPES'07, Cividale Del Friuli, Italy, 2-5 May 2007.
Program-ing in Coq. Matthieu Sozeau, Talk given at the ProVal seminar, Orsay, 9th march 2007.
Subset Coercions in Coq. Matthieu Sozeau, Talk given at TYPES'06, University of Nottingham, UK, 19-21 april 2006.

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.

Education

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++.