Matthieu Sozeau
where else to find them
what they talk about
where they keep going back
all 4 in the filters
on a stage with
all 17 in the filters
who talks about the same things
- Yannick Forster9 talks
- Théo Winterhalter14 talks
- Nicolas Tabareau14 talks
- Kenji Maillard11 talks
- Gabriel Claramunt4 talks
- Gilles Barthe17 talks
| title | conference | date |
|---|---|---|
| Session with the Rocq Development Team | RocqPL 2026 | 2026-01-17 |
Rocq releases 9.0 and 9.1 ship a single rag binary, a split of the standard library into a minimal core plus a separate stdlib, and fixes to the guard checker… | ||
| Nested Inductive Types for Rocq and Lean | RocqPL 2026 | 2026-01-17 |
Nested nested inductive types like RoseTree now get a syntactic check that classifies well behaved cases and rejects ones that rely on reduction tricks… | ||
| Enhancing universe polymorphism for Rocq: Algebraic universes, consistency checking(…) | RocqPL 2026 | 2026-01-17 |
Mechanical refinement of Bezem–Coquand’s decision procedure is implemented and machine-verified inside a Rocq branch, producing a concrete universe model and… | ||
| Bounded Sort Polymorphism with Elimination Constraints | POPL 2026 | 2026-01-11 |
Extends sort polymorphism with elimination constraints that record which sorts may eliminate into which, implements the system in the Rocq prover, and proves… | ||
| All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants | POPL 2025 | 2025-01-19 |
Adds a principled sort quantifier that generalizes Prop, Type, and SProp and is implemented in Coq with a new sort-polymorphic prelude that replaces duplicated… | ||
| Verified Extraction from Coq to OCaml | PLDI 2024 | 2024-06-24 |
A verified extraction pipeline implemented in Coq proves that programs over first‑order inductive data types extracted from Coq safely interoperate with OCaml… | ||
| Session with the Coq Development Team | CoqPL 2024 | 2024-01-20 |
Coq releases 8.17–8.19 add concrete features: ability to disable notations locally and use temporary scopes with an underscore, Ltac2 gains arrays, maps and… | ||
| Session with the Coq Development Team | CoqPL 2022 | 2022-01-22 |
Coq 8.14 and 8.15 introduce a new case representation change that fixes surprising match-occurrence bugs and a Metacoq-checked subject reduction proof; native… | ||
| Session with the Coq Development Team | CoqPL 2021 | 2021-01-19 |
Coq 8.13 appears: compile libraries with 8.13 to see new hint warnings and migrate by changing a hint’s attribute from global to export so it only activates… | ||
| Session with the Coq Development Team | POPL 2021 | 2021-01-17 |
Coq 8.13 ships with a new warning for hints and a staged migration: marking hints global preserves old behavior while the default will flip later, so compile… | ||
| An Equations Tutorial | CoqPL 2020 | 2020-01-25 |
Equations lets you write Coq functions by equations with rich pattern matching and recursion that elaborate to pure Gallina and generate a rewrite database of… | ||
| nothing matches | ||