Jonáš Fiala
where else to find them
what they talk about
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2023–2026
on a stage with
all 18 in the filters
who talks about the same things
- Aurel Bílý5 talks
- Markus de Medeiros3 talks
- Alexander J. Summers13 talks
- Ralf Jung18 talks
- Derek Dreyer35 talks
- Guido Martínez10 talks
| title | conference | date |
|---|---|---|
| Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic | PLDI 2026 | 2026-06-15 |
Kuiper is an F library that uses Pulse-based separation logic to verify GPU kernels, extending the logic with forall+ connective and located resources to model… | ||
| Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing(…) | OOPSLA 2025 | 2025-10-16 |
Place Capability Graphs (PCG) present a concretely computable model of Rust ownership that is extracted from the compiler’s MIR and borrow-checker facts and… | ||
| Kuiper: verified and efficient GPU programming | ARRAY 2025 | 2025-06-17 |
Kuiper is a verified GPU language that uses dependent types and concurrent separation logic (built on F★/Pulse) to guarantee memory safety and race freedom for… | ||
| Leveraging Rust Types for Program Synthesis | PLDI 2023 | 2023-06-17 |
First deductive synthesizer for safe Rust that uses Rust types to both shrink specifications and prune search, extracting programs from proofs and guaranteeing… | ||
| nothing matches | ||