Simon Spies

Publication Activity (10 Years)

Years Active: 2019-2024
Publications (10 Years): 9

Top Topics

Logical Language

Fixed Point Semantics

Abductive Inference

Top Venues

Proc. ACM Program. Lang.

Publications

Simon Spies, Lennard Gäher, Michael Sammler, Derek Dreyer
Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer
DimSum: A Decentralized Approach to Multi-language Semantics and Verification. Proc. ACM Program. Lang. 7 (POPL) (2023)
Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
Later credits: resourceful reasoning for the later modality. Proc. ACM Program. Lang. 6 (ICFP) (2022)
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer
Simuliris: a separation logic framework for verifying concurrent program optimizations. Proc. ACM Program. Lang. 6 (POPL) (2022)
Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. PLDI (2021)
Simon Spies, Neel Krishnaswami, Derek Dreyer
Transfinite step-indexing for termination. Proc. ACM Program. Lang. 5 (POPL) (2021)
Simon Spies, Yannick Forster
Undecidability of higher-order unification formalised in Coq. CPP (2020)
Yannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark
Call-by-push-value in coq: operational, equational, and denotational theory. CPP (2019)