Call-by-push-value in coq: operational, equational, and denotational theory. - Yannick Forster 002; Steven Schäfer; Simon Spies; Kathrin Stark (CPP, 2019)

Undecidability of higher-order unification formalised in Coq. - Simon Spies; Yannick Forster 002 (CPP, 2020)

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. - Simon Spies; Lennard Gäher; Daniel Gratzer; Joseph Tassarotti; Robbert Krebbers; Derek Dreyer; Lars Birkedal (PLDI, 2021)

Transfinite step-indexing for termination. - Simon Spies; Neel Krishnaswami; Derek Dreyer (Proc. ACM Program. Lang., 2021)

Simuliris: a separation logic framework for verifying concurrent program optimizations. - Lennard Gäher; Michael Sammler; Simon Spies; Ralf Jung 002; Hoang-Hai Dang; Robbert Krebbers; Jeehoon Kang; Derek Dreyer (Proc. ACM Program. Lang., 2022)

Later credits: resourceful reasoning for the later modality. - Simon Spies; Lennard Gäher; Joseph Tassarotti; Ralf Jung 002; Robbert Krebbers; Lars Birkedal; Derek Dreyer (Proc. ACM Program. Lang., 2022)

DimSum: A Decentralized Approach to Multi-language Semantics and Verification. - Michael Sammler; Simon Spies; Youngju Song; Emanuele D'Osualdo; Robbert Krebbers; Deepak Garg 001; Derek Dreyer (Proc. ACM Program. Lang., 2023)

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. - Armaël Guéneau; Johannes Hostert; Simon Spies; Michael Sammler; Lars Birkedal; Derek Dreyer (Proc. ACM Program. Lang., 2023)

Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq. - Simon Spies; Lennard Gäher; Michael Sammler; Derek Dreyer (Proc. ACM Program. Lang., 2024)

Destabilizing Iris. - Simon Spies; Niklas Mück; Haoyi Zeng; Michael Sammler; Andrea Lattuada 001; Peter Müller 001; Derek Dreyer (Proc. ACM Program. Lang., 2025)