*The Definitional Side of Forcing*in

*LICS*. Guilhem Jaber, Gabriel Lewertowsky, Pierre-Marie Pédrot, Matthieu Sozeau & Nicolas Tabareau. , April 2016.

News

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

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 [17]
and their relations to homotopy/cubical type theory.

- August: at the ITP 2016 conference and Coq Workshop 2016 in Nancy, where Hugo Herbelin passed me the Coq development coordinator hat [2].
- July: at the Categorical Logic & Univalent Foundations workshop in Leeds, talking about forcing [3]
- July: at ICMS'16, gave a talk on Coq for HoTT [4]
- June: at the DeepSpec kickoff meeting in Princeton, NJ, gave a talk on Coq 8.6 [5] and enjoyed a lot of Coq-related talks!
- May: at the second Coq implementors workshop in Nice, gave a talk on Universes [6] for ML hackers.
- April: our paper [17] 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 [8]
- January: Gave a talk [9] 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 [10] 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 [11] 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 [12] on Coq for proving functional programs at the "École de Printemps d'Informatique Théorique" in Fréjus.
- May 8th: Paper on Equations [13] and Predicative System F, joint work with Cyprien Mangin accepted at LFMTP'15.
- May: Paper [14] 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 [15] 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 [16].
- January: at POPL'15 in Mumbai, for the first CoqPL workshop, we released Coq 8.5 beta [17].
- December-March 2015: Lecturing on proof assistants at the MPRI.

- 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 [18], at ITP on universe polymorphism [19] and at the Coq workshop on rewriting strategies [20] and Coq 8.5 [21].
- May'14: I gave a seminar at the XIX AIM in Paris on universe polymorphism [22].
- Apr'14: Gave a seminar at the Deducteam HoTT working group on an Internalization of the Groupoid Model of Type Theory [23].
- Apr'14: Universe Polymorphism in Coq [24] to appear at ITP'14.
- Feb'14: Draft paper on an Internalization of the Groupoid Model of Type Theory [25].
- 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 [26] 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.

Copyright © 2006-2015 Matthieu Sozeau