You are on Matthieu Sozeau's website, that's me on the right. Commits are worth a thousand words on my github.

What's next

  • I will be coorganizing the EPIT 2020 Spring School with Nicolas Tabareau on Homotopy Type Theory, at Oléron, May 25-29 2020



  • December: I gave a seminar on programming with Coq [1] attached to Xavier Leroy's lectures on Curry-Howard Today at the Collège de France.
  • November: I gave a talk on our universe of strict propositions [2] and Eric Finster gave one on higher universal algebra in type theory at the PPS days.
  • October: I gave a talk on the MetaCoq Project [3] at the VALS seminar.
  • October: Definitional Proof-Irrelevance without K [4] has been accepted at POPL'19. We present a version of definitionally strict propositions compatible with univalent models. Soon to be found in Coq!
  • September-November: MPRI 2.7.2 lecture on proof assistants.
  • September: we got the distinguished paper award for our paper "Equivalences for Free!" [5] at ICFP'18.
  • September: I am part of the LSFA 2018 program comittee, which will happen in Fortaleza, Brazil in September 2018.
  • September: I am part of the TyDe 2018 program comittee colocated with ICFP 2018 in St. Louis, MI.
  • August: introductory lecture on Dependent Type Theory at the EUTYPES summer school 2018.
  • July: I was part of the ITP 2018 program comittee, and co-organizing the Coq Workshop at FLoC 2018.
  • June: I gave an invited talk [6] at the TYPES 2018 conference in Braga, Portugal, June 18-21.
  • April: I was an examiner of Amin Timany's PhD, who defended successfully his thesis in KU Leuven, Belgium.
  • April 26th: I gave a guest lecture [7] on dependent pattern-matching and Equations at the University of Saarland.
  • April 10-11th: participated in the pi.r2 days in Fontainebleau and gave a general talk on Coq as "An Environment for Programming with Dependent Types, take II". Our team is a quite interesting mix!
  • April: our paper on Cumulative Inductive Types [8] was accepted at FSCD'18.
  • April: our paper on Certified Meta-Programming with Typed Template Coq [9] was accepted at ITP'18.
  • March: submitted papers on Equations Reloaded [10], an effective ETT to ITT translation [11] and Equivalences for Free! to ICFP.
  • January: I attended the EUTypes meeting in Nijmegen where I gave a short talk on handling of recursion in Equations [12].
  • January: I attended POPL 2018, PEPM, CPP and CoqPL as well. Giving a presentation + poster at PEPM 2018 on Equations [13], a talk on Typed Template Coq [14] at CoqPL'18, along with the traditional Coq developer session [15].


  • November: participated to the Géocal-LAC days in Nantes, and gave a talk on cumulative inductives types [16].
  • October: Coq 8.7 was released, including cumulative inductive types. With Amin Timany, we proved the consistency [17] of this extension using a set-theoretic model.
  • October: released Equations version 1.0beta with a handful of examples, and submitted an article on the new version, joint work with Cyprien Mangin.
  • October: new article on deriving Equivalences for free with Nicolas Tabareau and Eric Tanter.
  • October: with Amin Timany, we proved the soundness of our extension of Coq with Cumulative Inductive Types.
  • September: Théo Winterhalter started his PhD in the CoqHoTT team, co-supervised with Nicolas Tabareau.
  • June: branching version 8.7 of Coq, which includes cumulative inductive types and integrates the ssreflect plugin.
  • June: gave a lecture at EJCP'17 on Type Theory and Interactive Theorem Proving in Coq [18]
  • June: at the 3rd Coq's Implementors Workshop in Carnac, Britany.
  • May: at TYPES 2017, for our work on cumulative inductive types [19].
  • March-April: working on Cumulative Inductive Types with Amin Timany, adding a cumulativity rule to inductives, simulating template polymorphism.
  • January-March: MPRI lecture on proof assistants.
  • January: Attended CPP 2017, POPL 2017 and CoqPL'17, and had a blast! Greg and Andrew presented our work on CertiCoq [20] there.


  • November: we released Coq version 8.6beta1: A Better, Faster, Stronger Rooster!
  • November: our paper [21] on the HoTT library got accepted at CPP 2017!.
  • November: our presentation on CertiCoq was accepted at CoqPL'17!
  • October: the extended version of our paper on was accepted at JFP.
  • August: at the ITP 2016 conference and Coq Workshop 2016 in Nancy, where Hugo Herbelin passed me the Coq development coordinator hat [22].
  • July: at the Categorical Logic & Univalent Foundations workshop in Leeds, talking about forcing [23]
  • July: at ICMS'16, gave a talk on Coq for HoTT [24]
  • June: at the DeepSpec kickoff meeting in Princeton, NJ, gave a talk on Coq 8.6 [25] and enjoyed a lot of Coq-related talks!
  • May: at the second Coq implementors workshop in Nice, gave a talk on Universes [26] for ML hackers.
  • April: our paper [27] on a new call-by-name forcing translation in Type Theory got accepted at LICS.
  • March: at the Dagstuhl seminar on "Language Based Verification Tools for Functional Programs", giving a short talk on Equations [28]
  • January: Gave a talk [29] at the CoqPL workshop on Coq 8.5
  • January: (finally!) released Coq 8.5, including my work on universe polymorphism and primitive projections.


  • December-March: Coq lecture at MPRI
  • September 1st: Gave a talk [30] on our work on unification with Beta Ziliani at ICFP'15.
  • August 1st: at the LFMTP'15 workshop, where Cyprien presented our work on Equations and Predicative System F.
  • June 27th-July 3rd: Gave a lecture [31] at the HoTT/UF workshop and attending TLCA'15 in Warsaw.
  • June 22-26: first successful Coq coding sprint in lovely Nice, followed by the Coq Workshop
  • June 1st: ERC CoqHoTT started!
  • May 26th: Gave a lecture [32] on Coq for proving functional programs at the "École de Printemps d'Informatique Théorique" in Fréjus.
  • May 8th: Paper on Equations [33] and Predicative System F, joint work with Cyprien Mangin accepted at LFMTP'15.
  • May: Paper [34] on a new unification algorithm for Coq, joint work with Beta Ziliani, accepted at ICFP'15. The Coq plugin is here.
  • April 29th: Gave a seminar [35] at MIT on our new unification algorithm.
  • April 22nd: Released Coq 8.5 beta 2.
  • March: Submitted a new version of our work with Nicolas on Internalizing Intensional Type Theory [36].
  • January: at POPL'15 in Mumbai, for the first CoqPL workshop, we released Coq 8.5 beta [37].
  • December-March 2015: Lecturing on proof assistants at the MPRI.
Programmer avec Coq: filtrage dépendant et récursion. Matthieu Sozeau, Séminaire au Collège de France, Paris, France, 12 Décembre 2018.
A Universe of Strict Propositions in Type Theory. Matthieu Sozeau, Talk given at the PPS Days, IRIF, Paris, France, November 2018.
The MetaCoq Project. Matthieu Sozeau, Talk given at the VALS Seminar, LRI, Gif-sur-Yvette, France, October 2018.
Definitional Proof-Irrelevance without K in 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019). Gilbert, Gaëtan, Cockx, Jesper, Sozeau, Matthieu & Tabareau, Nicolas. Lisbon, Portugal, January 2019.
Equivalences for Free in ICFP 2018 - International Conference on Functional Programming. Tabareau, Nicolas, Tanter, Éric & Sozeau, Matthieu. Saint-Louis, United States, September 2018, pp.1-29.
The Predicative, Polymorphic, Cumulative Calculus of Inductive Constructions and its implementation. Matthieu Sozeau, Invited talk at the TYPES 2018 conference, Braga, Portugal, June 20th 2018.
A Gentle Introduction to Equations Or How to Match Regexps with Dependently-Typed Continuations. Matthieu Sozeau, Lecture notes for a guest lecture given at Saarland University, Saarbrücken, Germany, April 2018.
Cumulative Inductive Types In Coq in 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK. Amin Timany & Matthieu Sozeau. , 2018, pp.29:1-29:16.
Towards Certified Meta-Programming with Typed Template-Coq in ITP 2018. Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau & Nicolas Tabareau. , 2018, pp.20-39.
Equations Reloaded. Cyprien Mangin & Matthieu Sozeau, Unpublished, July 2018 - In revision.
Eliminating Reflection from Type Theory. Winterhalter, Théo, Sozeau, Matthieu & Tabareau, Nicolas , October 2018 - Accepted at CPP'19.
Nested, Well-Founded and Mutual recursion in Equations. Matthieu Sozeau, Talk given at the EUTypes 2018 Working Meeting, Nijmegen, Netherlands, January 2018.
Equations: From Clauses to Splittings to Functions. Cyprien Mangin & Matthieu Sozeau, Talk and Poster at PEPM 2018 - ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Los Angeles, CA, USA, January 2018.
Typed Template Coq in CoqPL'18. Simon Boulier, Matthieu Sozeau, Nicolas Tabareau & Abhishek Anand. Los Angeles, CA, USA, January 2018.
Coq dev talk in CoqPL'18. Matthieu Sozeau, Maxime Dénès & Yves Bertot. Los Angeles, CA, USA, January 2018.
Cumulative Inductive Types in Coq. Matthieu Sozeau, Talk at Géocal-LAC days, Nantes, France, November 14th 2017.
Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC). Timany, Amin & Sozeau, Matthieu, Technical Report, KU Leuven, Belgium ; Inria Paris, October 2017, p.30.
Introduction to Type Theory and Interactive Theorem Proving in Coq. Matthieu Sozeau, Lecture notes for a course given at EJCP'17 in Toulouse, June 27th 2017.
Cumulative Inductive Types in Coq in TYPES 2017 Proceedings. Amin Timany, Matthieu Sozeau & Bart Jacobs. Budapest, Hungary, May 2017.
CertiCoq: A verified compiler for Coq in CoqPL. Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau & Matthew Weaver. Paris, France, January 2017.
The HoTT Library: A formalization of homotopy type theory in Coq. Bauer, A., Gross, J., LeFanu Lumsdaine, P., Shulman, M., Sozeau, M. & Spitters, B. ArXiv e-prints, October 2016 - Accepted at CPP'17.
Coq 8.6. Matthieu Sozeau, Talk at the Coq Workshop in Nancy, France, August 26th 2016.
Forcing Translations in Type Theory. Matthieu Sozeau, Invited talk at the Categorical Logic and Univalent Foundations workshop, Leeds, UK, July 28th 2016.
Coq for HoTT. Matthieu Sozeau, Invited talk at the International Conference on Mathematical Software in Berlin, Germany, July 14th 2016.
Coq 8.6. Maxime Dénès, Matthieu Sozeau, Talk at the DeepSpec Kickoff Workshop in Princeton, NJ, USA, June 8th 2016.
Universe Polymorphism for the OCaml hacker. Matthieu Sozeau, Talk at the Second Coq Implementors Workshop, Sophia-Antipolis, France, June 2nd 2016.
The Definitional Side of the Forcing in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016. Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau & Nicolas Tabareau. , 2016, pp.367-376.
Equations: a function definition toolbox for Coq. Matthieu Sozeau, Talk at Dagstuhl, March 2016.
Coq 8.5 at work. Maxime Dénès, Matthieu Sozeau, Talk given at the second CoqPL Workshop, St Petersburg, FL, January 2016.
A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading. Matthieu Sozeau, Talk given at ICFP'15, Vancouver, Canada, September 2015.
Coq support for HoTT. Matthieu Sozeau, Invited talk at the HoTT/UF workshop in Warsaw, Poland, June 2015.
Functional Programming and Proving in Coq. Matthieu Sozeau, Lecture at the "École de Printemps d'Informatique Théorique 2015" in Fréjus, France, May 2015.
Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study in Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice. Mangin, Cyprien & Sozeau, Matthieu. Volume 185 of EPTCS. , May 2015 - LFMTP'15.
A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading in ACM SIGPLAN International Conference on Functional Programming 2015. Beta Ziliani & Matthieu Sozeau. , 2015.
A Predictable Unification Algorithm for Coq. Matthieu Sozeau, Talk given at MIT, Cambridge, MA, April 29th 2015.
Internalizing Intensional Type Theory. Sozeau, Matthieu & Tabareau, Nicolas, Unpublished, February 2015.
Coq dev talk. Matthieu Sozeau, Talk given at the First CoqPL workshop, Mumbai, India, January 2015.
Valid XHTML 1.1! Valid CSS!