Yannick Forster
where else to find them
no profile links on file
what they talk about
where they keep going back
no series more than once — all 6 in the filters
on a stage with
all 6 in the filters
who talks about the same things
- Matthieu Sozeau14 talks
- Théo Winterhalter14 talks
- Gabriel Claramunt4 talks
- Yannick Zakowski11 talks
- Kathrin Stark8 talks
- Nicolas Tabareau14 talks
| title | conference | date |
|---|---|---|
| Code Generation via Meta-programming in Dependently Typed Proof Assistants | WITS 2026 | 2026-01-17 |
A survey implements seven implementations of a Functor-deriving meta program that generates the map function for option/list/tree and other boilerplate across… | ||
| 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… | ||
| 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… | ||
| A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive... | CPP 2023 | 2023-01-16 |
Paper proves a constructive Cantor–Bernstein for enumerable discrete types and gives three explicit bijection constructions: a Myhill-style staged build with… | ||
| MetaCoq as a tool to prevent future unsoundness in Coq | Unsound 2022 | 2022-12-06 |
MetaCoq formalizes Coq’s calculus inside Coq and provides verified implementations of core pieces of the kernel, aiming to catch soundness bugs before they… | ||
| A Coq Library of Undecidable Problems | CoqPL 2020 | 2020-01-25 |
A Coq library formalizes a large graph of undecidability reductions and actually produces executable artifacts: it mechanizes PCP, Hilbert’s tenth, first-order… | ||
| nothing matches | ||