Éric Tanter
where else to find them
bluesky:etanter.bsky.social
speakerdeck:etanter
what they talk about
all 7 in the filters
where they keep going back
all 5 in the filters
on a stage with
all 32 in the filters
who talks about the same things
- Nicolas Tabareau14 talks
- Kenji Maillard11 talks
- Matías Toro6 talks
- Théo Winterhalter14 talks
- Jonathan Aldrich17 talks
- Max S. New8 talks
| title | conference | date |
|---|---|---|
| Testing Incomplete Programs in OCaml | ML Family Workshop 2026 | 2026-08-28 |
Testing frameworks get a third verdict called incomplete that distinguishes unfinished code from real failures; small edits to Alcotest and QCheck make them… | ||
| 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… | ||
| 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… | ||
| Robust Dynamic Embedding for Gradual Typing | ICFP 2025 | 2025-10-12 |
Defines Robust Dynamic Embedding as a new adequacy criterion: if a dynamic component semantically satisfies a static type then its embedding ascribed to that… | ||
| 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… | ||
| Taming Unsoundness with Gradual Abstract Interpretation | UNSOUND 2024 | 2024-10-20 |
Proposes that optimistic but unsound assumptions in abstract interpretation become safe by automatically inserting runtime checks so analysis results are sound… | ||
| Securing Verified IO Programs Against Unverified Code in F* | POPL 2024 | 2024-01-14 |
A verified secure compilation pipeline for F programs that perform IO, called SCIO, compiles verified code to a smaller F target and enforces assumptions at… | ||
| Plausible sealing for gradual parametricity | OOPSLA 2022 | 2022-12-05 |
Proposes plausible sealing: postpone sealing decisions by inserting “maybe-seal” evidence so runtime, not static imprecision, decides whether a value is… | ||
| 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… | ||
| Propositional Equality for Gradual Dependently Typed Programming | ICFP 2022 | 2022-09-11 |
A gradual dependently-typed language is implemented that adds a propositional equality whose proofs carry witnesses (each proof pairs an equality with a term… | ||
| Gradually Structured Data | OOPSLA 2021 | 2021-10-17 |
A formal core language for “gradually structured data” introduces open and closed algebraic datatypes, two new runtime types—unknown datatype and unknown open… | ||
| Gradual Verification of Recursive Heap Data Structures | OOPSLA 2020 | 2020-11-15 |
Practical system that extends a base static verifier with gradual formulas and optimistic strengthening, inserting runtime checks when a missing spec was… | ||
| nothing matches | ||