Cyril Cohen
where else to find them
what they talk about
where they keep going back
no series more than once — all 3 in the filters
on a stage with
- Ayumu Saitoonce
- Kazuhiko Sakaguchionce
- Reynald Affeldtonce
all 4 in the filters
who talks about the same things
nobody close enough yet
| title | conference | date |
|---|---|---|
| Implementing parametricity in Rocq-ELPI | RocqPL 2026 | 2026-01-17 |
Implements a sequent-calculus style binary parametricity as a logic program inside Rocq-ELPI, translating each inference rule to an ELPI clause that produces… | ||
| A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free | ICFP 2025 | 2025-10-12 |
Proves that a mergesort implementation satisfying a specific characteristic property yields correctness (sorted + permutation) and stability, for many… | ||
| Semantics of Probabilistic Programs using S-Finite Kernels in Coq | CPP 2023 | 2023-01-16 |
Extends a Coq formalization of measure and integration by adding s-finite kernels to interpret typing judgments for a probabilistic language, and proves key… | ||
| nothing matches | ||