All Stories

  1. Types Are Internal ∞-Groupoids

    Article • June 2021, Institute of Electrical & Electronics Engineers (IEEE)

    Dr Matthieu Sozeau

  2. The Marriage of Univalence and Parametricity

    Article • Journal of the ACM, February 2021, ACM (Association for Computing Machinery)

    Dr Matthieu Sozeau

  3. Coq Coq correct! verification of type checking and erasure for Coq, in Coq

    Article • Proceedings of the ACM on Programming Languages, January 2020, ACM (Association for Computing Machinery)

    Dr Matthieu Sozeau

  4. Equations reloaded: high-level dependently-typed functional programming and proving in Coq

    Article • Proceedings of the ACM on Programming Languages, July 2019, ACM (Association for Computing Machinery)

    Dr Matthieu Sozeau

  5. Definitional proof-irrelevance without K

    Article • Proceedings of the ACM on Programming Languages, January 2019, ACM (Association for Computing Machinery)

    Dr Matthieu Sozeau

  6. Equivalences for free: univalent parametricity for effective transport

    Article • Proceedings of the ACM on Programming Languages, July 2018, ACM (Association for Computing Machinery)

    Dr Matthieu Sozeau

  7. A unification algorithm for Coq featuring universe polymorphism and overloading

    Article • ACM SIGPLAN Notices, December 2015, ACM (Association for Computing Machinery)

    Dr Matthieu Sozeau

  8. A unification algorithm for Coq featuring universe polymorphism and overloading

    Article • August 2015, ACM (Association for Computing Machinery)

    Dr Matthieu Sozeau

  9. Partiality and recursion in interactive theorem provers – an overview

    Article • Mathematical Structures in Computer Science, November 2014, Cambridge University Press

    Dr Matthieu Sozeau