*Internalization of the Groupoid Interpretation of Homotopy Type Theory*. Sozeau, Matthieu & Tabareau, Nicolas, Unpublished, February 2014 - Submitted.

News

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 [1].
- Jan-Feb'14: Lecturing on proof asssitants at the MPRI.
- Jan'14: Submitted a paper on Universe Polymorphism in Coq [2].
- Jan'14: Gave a talk [3] 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 [4] on unification and subtyping for universe polymorphism at the Typex meeting.
- Nov'13: Gave a seminar [5] on universe polymorphism at the Coq working group.
- Jun'13: The HoTT book [6] has been released!
- Apr'13: Gave a talk at TYPES'13 on universe polymorphism. [7]
- 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 [8] with a nice exercise.
- July'12: At LICS in Croatia with N. Tabareau and G. Jaber for our paper on Forcing in Type Theory [9].

*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.

*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.

*Extending Type Theory with Forcing*in

*Proceedings of LICS'12*. Jaber, Guilhem, Tabareau, Nicolas & Sozeau, Matthieu.