François Pottier
where else to find them
what they talk about
all 4 in the filters
where they keep going back
all 6 in the filters
on a stage with
all 24 in the filters
who talks about the same things
- Alexandre Moine8 talks
- Jean-Marie Madiot2 talks
- Jacques-Henri Jourdan4 talks
- Michael Sammler16 talks
- Arthur Charguéraud7 talks
- Amin Timany16 talks
| title | conference | date |
|---|---|---|
| Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage(…) | POPL 2026 | 2026-01-11 |
IrisFit is a separation logic, formalized in Coq on top of the Iris framework, that uses space credits to bound heap usage for a concurrent call-by-value… | ||
| Formal Semantics and Program Logics for a Fragment of OCaml | ICFP 2025 | 2025-10-12 |
Defines OLang, a sequential OCaml fragment with first-class functions, extensible ADTs, pattern matching, references, exceptions and effect handlers, and gives… | ||
| Data Race Freedom à la Mode | POPL 2025 | 2025-01-19 |
DRFcaml extends OCaml's type system with new mode axes (contention and portability) to statically guarantee data-race freedom for multi-threaded OCaml while… | ||
| Tail Modulo Cons, OCaml, and Relational Separation Logic | POPL 2025 | 2025-01-19 |
Implements Tail Modulo Constructor in the OCaml compiler and shows it reliably turns non‑tail List.map‑style definitions into stack‑safe code; proof of… | ||
| Type Inference Logics | OOPSLA 2024 | 2024-10-20 |
Shows how to verify practical, imperative-style, constraint-based type inference that emits elaborated terms by separating constraint generation (implemented… | ||
| Thunks and Debits in Separation Logic with Time Credits | POPL 2024 | 2024-01-14 |
Machine‑checked reconstruction of Okasaki’s debit reasoning implemented in Iris$, with proofs and reusable artifacts (Zenodo/GitLab). Formalizes the missing… | ||
| Osiris: an Iris-based program logic for OCaml | OCaml 2023 | 2023-09-09 |
Osiris provides an Iris-based program logic inside Coq to verify OCaml modules by translating OCaml ASTs into a deep-embedded Coq representation and proving an… | ||
| A High-Level Separation Logic for Heap Space under Garbage Collection | POPL 2023 | 2023-01-15 |
Logic gives a concrete way to prove heap-space bounds under a GC that follows the free-variable rule: allocation consumes space credits, deallocation returns… | ||
| Specification and Verification of a Transient Stack | CPP 2022 | 2022-01-17 |
Defines and machine-verified a scaled-down transient stack implemented as a list of fixed-capacity chunks with unique identifiers for ownership, copy‑on‑write… | ||
| A Separation Logic for Heap Space under Garbage Collection | POPL 2022 | 2022-01-16 |
A separation logic (called SLgc in the paper) models heap space under tracing GC by treating allocation budget as space credits consumed on allocation and… | ||
| Faster Reachability Analysis for LR(1) Parsers | SLE 2021 | 2021-10-17 |
A new algorithm reframes LR(1) reachability as recursive matrix equations (using the min,+ semiring) and replaces Pottier 2016 with a naive cost matrices… | ||
| A Separation Logic for Effect Handlers | POPL 2021 | 2021-01-17 |
Introduces a Separation Logic that embeds protocols into Iris-style weakest preconditions to specify and verify programs using user-defined effect handlers… | ||
| Cosmo: A Concurrent Separation Logic for Multicore Ocaml | ICFP 2020 | 2020-08-23 |
Cosmo provides a separation logic for Multicore OCaml that exposes the weak memory model yet lets you verify familiar locks: it instantiates Iris and is… | ||
| nothing matches | ||