Internalization of the Groupoid Interpretation of Homotopy Type Theory. Sozeau, Matthieu & Tabareau, Nicolas, Unpublished, February 2014 - Submitted.
Commits are worth a thousand words on my github.
I'll be at the semester at IHP starting in spring and ITP-4. I'm organizing the TYPES'14 conference in Paris this spring, submit!
- Feb'14: Submitted a paper on an Internalization of the Groupoid Model of HoTT .
- Jan-Feb'14: Lecturing on proof asssitants at the MPRI.
- Jan'14: Submitted a paper on Universe Polymorphism in Coq .
- Jan'14: Gave a talk  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.
- Dec'13: Gave a talk  on unification and subtyping for universe polymorphism at the Typex meeting.
- Nov'13: Gave a seminar  on universe polymorphism at the Coq working group.
- Jun'13: The HoTT book  has been released!
- Apr'13: Gave a talk at TYPES'13 on universe polymorphism. 
- Mar'13: Gave a seminar on univalence for free at the Types and Realizability working group.
- Feb'13: Gave two lectures at the MPRI, on typeclasses and dependently-typed programming.
- Feb'13: Together with Nicolas Tabareau, we wrote an article on univalence and 2-groupoids, submitted .
- Feb'13: At the JFLA'13 in Aussois.
- Sep-Dec'12: At the IAS in Princeton, NJ for the special year on Homotopy type theory. Working specifically on universe polymorphism.
- October'12: Gave a lecture at UPenn on type classes  with a nice exercise.
- July'12: At LICS in Croatia with N. Tabareau and G. Jaber for our paper on Forcing in Type Theory .
Universe Polymorphism in Coq. Matthieu Sozeau & Nicolas Tabareau, Unpublished, January 2014 - Submitted.
Coq - Recent History. Matthieu Sozeau, SIGPLAN Programming Language Software Award 2013 talk, at POPL'14, San Diego, January 23rd 2014.
Universe Polymorphism: Subtyping and Unification. Matthieu Sozeau, Talk given at the Typex Meeting, Paris, December 17th 2013.
Universe Polymorphism and Fast Projections. Matthieu Sozeau, Talk given at the Coq Working Group, Paris, France.
Homotopy Type Theory: Univalent Foundations for Mathematics. The Univalent Foundations Program. Institute for Advanced Study, 2013.
Universe Polymorphism and Inference in Coq. Matthieu Sozeau, Talk given at TYPES'13, Toulouse, France, April 25th 2013.
Coq with Classes. Matthieu Sozeau, Lecture at the "Advanced Martial Arts in Coq" course at University of Pennsylvania, October 2012.