Simon Spies
where else to find them
no profile links on file
what they talk about
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2024–2025
- POPL2 editions2022–2023
all 5 in the filters
on a stage with
all 18 in the filters
who talks about the same things
- Michael Sammler16 talks
- Lennard Gäher7 talks
- Amin Timany16 talks
- Derek Dreyer35 talks
- Lars Birkedal35 talks
- Thibault Dardinier9 talks
| title | conference | date |
|---|---|---|
| Destabilizing Iris | PLDI 2025 | 2025-06-16 |
Adds Daenerys to Iris: a reworked resource layer that introduces unstable resources and an explicit frame modality, plus an unstable points-to and a… | ||
| Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq | PLDI 2024 | 2024-06-24 |
Quiver claims automated inference of full separation logic specs for C code while verifying soundness in Coq using Iris, implemented as a prototype atop… | ||
| Melocoton: A Program Logic for Verified Interoperability Between OCaml and C | OOPSLA 2023 | 2023-10-23 |
Melocoton claims the first formal semantics of the OCaml FFI and the first multi‑language program logic that reasons about OCaml and C interactions… | ||
| DimSum: A Decentralized Approach to Multi-language Semantics and Verification | POPL 2023 | 2023-01-15 |
DimSum presents a decentralized method that avoids fixing a source language, memory model, or closed set of languages by giving each language a… | ||
| Later Credits: Resourceful Reasoning for the Later Modality | ICFP 2022 | 2022-09-11 |
Introduces later credits as an ownable resource in Iris that splits stepping into a credit-generation rule and a credit-spending rule, letting proofs prepay… | ||
| Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz | POPL 2022 | 2022-01-16 |
Framework claims a mechanically checked simulation that preserves contextual refinement and termination under a fair scheduler for real concurrent compiler… | ||
| Undecidability of Higher-Order Unification Formalised in Coq | CPP 2020 | 2020-01-20 |
Mechanisation in Coq proves that second-order unification is undecidable and, via a conservative embedding, that all higher-order unification problems are… | ||
| nothing matches | ||