Kenji Maillard
where else to find them
what they talk about
where they keep going back
- POPL2 editions2025–2026
all 6 in the filters
on a stage with
all 17 in the filters
who talks about the same things
- Nicolas Tabareau14 talks
- Éric Tanter12 talks
- Théo Winterhalter14 talks
- Danel Ahman7 talks
- Sharon Shoham13 talks
- Tomas Diaz6 talks
| title | conference | date |
|---|---|---|
| Sulfur: Substitution Generation using a Logical Framework | RocqPL 2026 | 2026-01-17 |
A Coq/Rocq plugin reimplements Autosubst’s costly asimpl by reflective tactic reification: it generates concrete de Bruijn-based syntax, translates terms into… | ||
| 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… | ||
| AdapTT: Functoriality for Dependent Type Casts | POPL 2026 | 2026-01-11 |
A new type theory AdapTT formalizes adapters as external morphisms that form a category and lets every type former act functorially on those adapters so casts… | ||
| Incremental Certified Programming | OOPSLA 2025 | 2025-10-16 |
Claims a formal framework that makes specifications monotone over partial programs by defining a completion refinement relation and a notion of completeness… | ||
| 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… | ||
| Martin-Löf à la Coq | CPP 2024 | 2024-01-15 |
A Coq formalization of Martin-Löf Type Theory (MLTT) that mechanizes its metatheory and proves decidability of conversion and of type checking using… | ||
| Temporal refinements for Call-By-Push-Value with fixpoint | HOPE 2022 | 2022-09-11 |
Proposes temporal refinements for a Call-By-Push-Value calculus with arbitrary fixpoints and shows how a comonadic modality (a box) plus a later modality… | ||
| A Reasonably Gradual Type Theory | ICFP 2022 | 2022-09-11 |
Presents GRIP, an extension of CastCIC that is normalizing and a conservative extension of CIC, and that internalizes precision so graduality can be proven for… | ||
| nothing matches | ||