News
me
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'll be at POPL 2017 and CoqPL'17.

What I'm up to now

Currently, I'm playing with Induction-Induction and Induction-Recursion in Coq with Pierre-Évariste Dagand and CoqHoTT members, and generalizing generalized rewriting with Jérémie Koenig's logical relation library. With C. Mangin we're looking at making Equations more expressive, fast and robust. With G. Lewertowski and CoqHoTT members we're looking at forcing translations of type theory [19] and their relations to homotopy/cubical type theory.

Timeline/Log

2016

  • November: we released Coq version 8.6beta1: A Better, Faster, Stronger Rooster!
  • November: our paper [2] 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 unification [3] 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 [4].
  • July: at the Categorical Logic & Univalent Foundations workshop in Leeds, talking about forcing [5]
  • July: at ICMS'16, gave a talk on Coq for HoTT [6]
  • June: at the DeepSpec kickoff meeting in Princeton, NJ, gave a talk on Coq 8.6 [7] and enjoyed a lot of Coq-related talks!
  • May: at the second Coq implementors workshop in Nice, gave a talk on Universes [8] for ML hackers.
  • April: our paper [19] 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 [10]
  • January: Gave a talk [11] at the CoqPL workshop on Coq 8.5
  • January: (finally!) released Coq 8.5, including my work on universe polymorphism and primitive projections.

2015

  • December-March: Coq lecture at MPRI
  • September 1st: Gave a talk [12] 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 [13] 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 [14] on Coq for proving functional programs at the "École de Printemps d'Informatique Théorique" in Fréjus.
  • May 8th: Paper on Equations [15] and Predicative System F, joint work with Cyprien Mangin accepted at LFMTP'15.
  • May: Paper [16] 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 [17] 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 [18].
  • January: at POPL'15 in Mumbai, for the first CoqPL workshop, we released Coq 8.5 beta [19].
  • December-March 2015: Lecturing on proof assistants at the MPRI.

2014

  • November: ERC Starting Grant CoqHoTT got granted! Led by Nicolas Tabareau, it will explore the use of Coq for Homotopy Type Theory.
  • October: teaching formal methods of verification at Paris 7.
  • September'14: at ICFP'14 as part of the SRC and the Heidelberg Laureate Forum.
  • July'14: during the Vienna Summer of Logic, I gave talks at the UNIF workshop on unification in Coq [20], at ITP on universe polymorphism [21] and at the Coq workshop on rewriting strategies [22] and Coq 8.5 [23].
  • May'14: I gave a seminar at the XIX AIM in Paris on universe polymorphism [24].
  • Apr'14: Gave a seminar at the Deducteam HoTT working group on an Internalization of the Groupoid Model of Type Theory [25].
  • Apr'14: Universe Polymorphism in Coq [26] to appear at ITP'14.
  • Feb'14: Draft paper on an Internalization of the Groupoid Model of Type Theory [27].
  • Jan-Feb'14: Lecturing on proof assistants at the MPRI. My page about the lecture with links to slides and solutions to the exercises.
  • Jan'14: Gave a talk [28] with Gérard Huet at POPL'14 for the reception of the 2013 ACM SIGPLAN Software Systems Award by the Coq team.
  • Jan'14: Thanks developers and users for a (first, secret,) great Coq Users Meeting at POPL'14, the minutes are available. Looking forward to next year's meeting in Bombay!
  • Jan'14: At JFLA'14 and the SMC week on Recent developments in Type Theory in Lyon.
1
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.
2
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.
4
Coq 8.6. Matthieu Sozeau, Talk at the Coq Workshop in Nancy, France, August 26th 2016.
5
Forcing Translations in Type Theory. Matthieu Sozeau, Invited talk at the Categorical Logic and Univalent Foundations workshop, Leeds, UK, July 28th 2016.
6
Coq for HoTT. Matthieu Sozeau, Invited talk at the International Conference on Mathematical Software in Berlin, Germany, July 14th 2016.
7
Coq 8.6. Maxime Dénès, Matthieu Sozeau, Talk at the DeepSpec Kickoff Workshop in Princeton, NJ, USA, June 8th 2016.
8
Universe Polymorphism for the OCaml hacker. Matthieu Sozeau, Talk at the Second Coq Implementors Workshop, Sophia-Antipolis, France, June 2nd 2016.
9
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.
10
Equations: a function definition toolbox for Coq. Matthieu Sozeau, Talk at Dagstuhl, March 2016.
11
Coq 8.5 at work. Maxime Dénès, Matthieu Sozeau, Talk given at the second CoqPL Workshop, St Petersburg, FL, January 2016.
12
A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading. Matthieu Sozeau, Talk given at ICFP'15, Vancouver, Canada, September 2015.
13
Coq support for HoTT. Matthieu Sozeau, Invited talk at the HoTT/UF workshop in Warsaw, Poland, June 2015.
14
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.
15
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.
16
A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading in ACM SIGPLAN International Conference on Functional Programming 2015. Beta Ziliani & Matthieu Sozeau. , 2015.
17
A Predictable Unification Algorithm for Coq. Matthieu Sozeau, Talk given at MIT, Cambridge, MA, April 29th 2015.
18
Internalizing Intensional Type Theory. Sozeau, Matthieu & Tabareau, Nicolas, Unpublished, February 2015 - Submitted.
19
Coq dev talk. Matthieu Sozeau, Talk given at the First CoqPL workshop, Mumbai, India, January 2015.
20
Towards A Better Behaved Unification Algorithm for Coq. Matthieu Sozeau, Talk given at the UNIF workshop, Vienna, Austria, July 2014.
21
Universe Polymorphism in Coq. Matthieu Sozeau, Talk at ITP'14, Vienna, Austria, July 16th 2014.
22
Proof-relevant rewriting strategies. Matthieu Sozeau, Talk given at the Sixth Coq Workshop, Vienna, Austria, July 2014.
23
Coq 8.5: What's New, What's Next?. Matthieu Sozeau, Talk given at the Sixth Coq Workshop, Vienna, Austria, July 2014.
24
Universe Polymorphism: Subtyping and Unification. Matthieu Sozeau, Invited talk at the Agda Implementers Meeting, Paris, France, May 27th 2014.
25
Towards an Internalization of the Groupoid Model of Type Theory. Sozeau, Matthieu & Tabareau, Nicolas, Misc, April 2014.
26
Universe Polymorphism in Coq in ITP'14. Matthieu Sozeau & Nicolas Tabareau. Vienna, Austria, 2014 - To appear.
27
Towards an Internalization of the Groupoid Model of Type Theory. Sozeau, Matthieu & Tabareau, Nicolas, Unpublished, February 2014 - Under revision.
28
Coq - Recent History. Matthieu Sozeau, SIGPLAN Programming Language Software Award 2013 talk, at POPL'14, San Diego, January 23rd 2014.
Valid XHTML 1.1! Valid CSS!