All Stories

  1. Nested Inductive Types: Justified and Usable Nested Inductive Types in Lean and Rocq

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

    Dr Matthieu Sozeau

  2. Bounded Sort Polymorphism with Elimination Constraints

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

    Dr Matthieu Sozeau

  3. All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants

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

    Dr Matthieu Sozeau

  4. Correct and Complete Type Checking and Certified Erasure for Coq, in Coq

    Article • Journal of the ACM, November 2024, ACM (Association for Computing Machinery)

    Dr Matthieu Sozeau

  5. Verified Extraction from Coq to OCaml

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

    Dr Matthieu Sozeau

  6. Types Are Internal ∞-Groupoids

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

    Dr Matthieu Sozeau

  7. The Marriage of Univalence and Parametricity

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

    Dr Matthieu Sozeau

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

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

  10. Definitional proof-irrelevance without K

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

    Dr Matthieu Sozeau

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

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

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

    Dr Matthieu Sozeau

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

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

    Dr Matthieu Sozeau

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

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

    Dr Matthieu Sozeau