News
me
You are on Matthieu Sozeau's website, that's me on the right. Commits are worth a thousand words on my github.
I'll also be at ICFP'15 at the end of August.

2015

  • June 27th-July 3rd: Gave a lecture [1] 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
  • May 26th: Gave a lecture [2] on Coq for proving functional programs at the "École de Printemps d'Informatique Théorique" in Fréjus.
  • May 8th: Submitted a paper on Equations [3] and Predicative System F, joint work with Cyprien Mangin.
  • May: Paper [4] on a new unification algorithm for Coq accepted at ICFP'15, the Coq plugin is here.
  • April 29th: Gave a seminar [5] 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 [6].
  • January: at POPL'15 in Mumbai, for the first CoqPL workshop, we released Coq 8.5 beta [7].
  • 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 [8], at ITP on universe polymorphism [9] and at the Coq workshop on rewriting strategies [10] and Coq 8.5 [11].
  • May'14: I gave a seminar at the XIX AIM in Paris on universe polymorphism [12].
  • Apr'14: Gave a seminar at the Deducteam HoTT working group on an Internalization of the Groupoid Model of Type Theory [13].
  • Apr'14: Universe Polymorphism in Coq [14] to appear at ITP'14.
  • Feb'14: Draft paper on an Internalization of the Groupoid Model of Type Theory [15].
  • 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 [16] 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
Coq support for HoTT. Matthieu Sozeau, Invited talk at the HoTT/UF workshop in Warsaw, Poland, June 2015.
2
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.
3
Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study. Mangin, Cyprien & Sozeau, Matthieu, Unpublished, May 2015 - Submitted.
4
A Predictable Unification Algorithm for Coq featuring Universe Polymorphism and Overloading. Beta Ziliani & Matthieu Sozeau, Unpublished, February 2015 - Accepted at ICFP 2015.
5
A Predictable Unification Algorithm for Coq. Matthieu Sozeau, Talk given at MIT, Cambridge, MA, April 29th 2015.
6
Internalizing Intensional Type Theory. Sozeau, Matthieu & Tabareau, Nicolas, Unpublished, February 2015 - Submitted.
7
Coq dev talk. Matthieu Sozeau, Talk given at the First CoqPL workshop, Mumbai, India, January 2015.
8
Towards A Better Behaved Unification Algorithm for Coq. Matthieu Sozeau, Talk given at the UNIF workshop, Vienna, Austria, July 2014.
9
Universe Polymorphism in Coq. Matthieu Sozeau, Talk at ITP'14, Vienna, Austria, July 16th 2014.
10
Proof-relevant rewriting strategies. Matthieu Sozeau, Talk given at the Sixth Coq Workshop, Vienna, Austria, July 2014.
11
Coq 8.5: What's New, What's Next?. Matthieu Sozeau, Talk given at the Sixth Coq Workshop, Vienna, Austria, July 2014.
12
Universe Polymorphism: Subtyping and Unification. Matthieu Sozeau, Invited talk at the Agda Implementers Meeting, Paris, France, May 27th 2014.
13
Towards an Internalization of the Groupoid Model of Type Theory. Sozeau, Matthieu & Tabareau, Nicolas, Misc, April 2014.
14
Universe Polymorphism in Coq in ITP'14. Matthieu Sozeau & Nicolas Tabareau. Vienna, Austria, 2014 - To appear.
15
Towards an Internalization of the Groupoid Model of Type Theory. Sozeau, Matthieu & Tabareau, Nicolas, Unpublished, February 2014 - Under revision.
16
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!