News
me
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].
1
Internalization of the Groupoid Interpretation of Homotopy Type Theory. Sozeau, Matthieu & Tabareau, Nicolas, Unpublished, February 2014 - Submitted.
2
Universe Polymorphism in Coq. Matthieu Sozeau & Nicolas Tabareau, Unpublished, January 2014 - Submitted.
3
Coq - Recent History. Matthieu Sozeau, SIGPLAN Programming Language Software Award 2013 talk, at POPL'14, San Diego, January 23rd 2014.
4
Universe Polymorphism: Subtyping and Unification. Matthieu Sozeau, Talk given at the Typex Meeting, Paris, December 17th 2013.
5
Universe Polymorphism and Fast Projections. Matthieu Sozeau, Talk given at the Coq Working Group, Paris, France.
6
Homotopy Type Theory: Univalent Foundations for Mathematics. The Univalent Foundations Program. Institute for Advanced Study, 2013.
7
Universe Polymorphism and Inference in Coq. Matthieu Sozeau, Talk given at TYPES'13, Toulouse, France, April 25th 2013.
8
Coq with Classes. Matthieu Sozeau, Lecture at the "Advanced Martial Arts in Coq" course at University of Pennsylvania, October 2012.
9
Extending Type Theory with Forcing in Proceedings of LICS'12. Jaber, Guilhem, Tabareau, Nicolas & Sozeau, Matthieu. Dubrovnik, Croatie, June 2012.
Valid XHTML 1.1! Valid CSS!