Jonathan Protzenko
where else to find them
x:_protz_
what they talk about
all 5 in the filters
where they keep going back
- ICFP2 editions2022–2023
all 5 in the filters
on a stage with
all 32 in the filters
who talks about the same things
- Aymeric Fromherz9 talks
- Cătălin Hriţcu16 talks
- Guido Martínez10 talks
- Bryan Parno22 talks
- Exequiel Rivas6 talks
- Danel Ahman7 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… | ||
| 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… | ||
| Formalising Criminal Law in Catala | ProLaLa 2023 | 2023-01-15 |
Formalisation uses the Catala DSL to implement a DUI fine calculator for Florida law that inputs blood alcohol, prior DUI dates and damage and outputs min/max… | ||
| Aeneas: Rust Verification by Functional Translation | ICFP 2022 | 2022-09-11 |
Aeneas translates a large, safe subset of Rust (no interior mutability or unsafe) into a pure lambda calculus so proofs avoid memory/address reasoning… | ||
| Full Workshop | ML 2021 | 2021-08-26 |
A fast tour of research tools and case studies from ML 2021: a running effect-handler Unix model that composes write/exit/su/fork/interrupt handlers and… | ||
| nothing matches | ||