Look no further for my bibtex entries. All my papers and slides are available from this directory.



International Conferences

  • Eliminating reflection from type theory in Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019. Théo Winterhalter, Matthieu Sozeau & Nicolas Tabareau. , 2019, pp.91-103.
  • Cumulative Inductive Types In Coq in 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK. Amin Timany & Matthieu Sozeau. , 2018, pp.29:1-29:16.
  • Towards Certified Meta-Programming with Typed Template-Coq in ITP 2018. Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau & Nicolas Tabareau. Springer, July 2018, pp.20-39.
  • The HoTT library: a formalization of homotopy type theory in Coq in Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau & Bas Spitters. ACM, 2017, pp.164-172.
  • The Definitional Side of the Forcing in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016. Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau & Nicolas Tabareau. , 2016, pp.367-376.
  • A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading in ACM SIGPLAN International Conference on Functional Programming 2015. Beta Ziliani & Matthieu Sozeau. , 2015.
  • Universe Polymorphism in Coq in Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. Matthieu Sozeau & Nicolas Tabareau. , 2014, pp.499-514.
  • Extending Type Theory with Forcing in Proceedings of LICS'12. Jaber, Guilhem, Tabareau, Nicolas & Sozeau, Matthieu. Dubrovnik, Croatie, June 2012.
  • Equations: A Dependent Pattern-Matching Compiler in First International Conference on Interactive Theorem Proving. Matthieu Sozeau. Springer, July 2010.
  • First-Class Type Classes in TPHOLs. Matthieu Sozeau & Nicolas Oury. Otmane Ait Mohamed, César Muñoz and Sofiène Tahar (Eds). Volume 5170 of LNCS. Springer, August 2008, pp.278-293.
  • Program-ing Finger Trees in Coq in ICFP'07. Matthieu Sozeau. Freiburg, Germany: ACM Press, 2007, pp.13-24.
  • Subset Coercions in Coq in TYPES'06. Matthieu Sozeau. Thorsten Altenkirch and Conor McBride (Eds). Volume 4502 of Lecture Notes in Computer Science. Springer, 2007, pp.237-252.
International Workshops

National Conferences


Research Reports


Manuals and Tutorials

Invited Talks and Seminars

Valid XHTML 1.1! Valid CSS!