Aymeric Fromherz
where else to find them
what they talk about
all 5 in the filters
where they keep going back
- ICFP2 editions2020–2023
all 5 in the filters
on a stage with
all 27 in the filters
who talks about the same things
- Jonathan Protzenko8 talks
- Danel Ahman7 talks
- Aseem Rastogi7 talks
- Guido Martínez10 talks
- Nikhil Swamy14 talks
- Cătălin Hriţcu16 talks
| title | conference | date |
|---|---|---|
| Project Everest: Perspectives from Developing Industrial-Grade High-Assurance(…) | PLDI 2026 | 2026-06-15 |
Project Everest produces a verified TLS stack and crypto suite rather than promises: it yields 1.3 million lines of F source that build in two hours, emits… | ||
| StarMalloc: Verifying a Modern, Hardened Memory Allocator | OOPSLA 2024 | 2024-10-20 |
StarMalloc is a verified, concurrent, hardened user-space allocator implemented in F/Steel, extracted to C and proven functionally correct relative to a… | ||
| Programming contest report | ICFP 2023 | 2023-09-04 |
ICFP 2023 programming contest optimizes musician placement on a rectangular stage with blocking by other musicians and pillars, attendees (500–3,000) having… | ||
| Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verifica... | ICFP 2023 | 2023-09-04 |
Implements a userland F metaprogram that performs whole-call-graph code specialization for Low and compiles to readable C, producing an extra compiler stage… | ||
| FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores | CPP 2023 | 2023-01-16 |
FastVer2 is a verified, concurrent monitor for the Faster key-value store: implemented in C (≈8,000 lines produced from ≈50,000 lines of F proofs) using the… | ||
| Turning Catala into a Proof Platform for the Law | Programming Languages and the Law 2022 (ProLaLa 2022) | 2022-01-16 |
Catala becomes a proof platform that uses proof-by-refinement to simplify programs while preserving semantics, generating no-empty/no-conflict VCs for default… | ||
| SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed ... | ICFP 2020 | 2020-08-23 |
SteelCore provides a semantics for CSL inside F, deriving Hoare rules from effectful non‑deterministic interleaving; it encodes computations as action trees… | ||
| nothing matches | ||