Hi, I'm Simon Spies.

I am currently a software engineer in London working on the OCaml compiler.

Before that, I did my PhD with Derek Dreyer at the Max Planck Institute for Software Systems and Saarland University. And before that, I obtained my Master's degree from the University of Cambridge and my Bachelor's degree from Saarland University.

You can reach me at last name at mpi-sws.org.

Publications

1. Destabilizing Iris

   Simon Spies, Niklas Mück, Haoyi Zeng, Michael Sammler, Andrea Lattuada, Peter Müller, Derek Dreyer

   46th ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2025, Seoul, South Korea

   Distinguished Paper Award

   PDF Website Talk

2. Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq

   Simon Spies, Lennard Gäher, Michael Sammler, Derek Dreyer

   45th ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2024, Copenhagen, Denmark

   Distinguished Artifact Award

   PDF Website Talk

3. 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

   38th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2023, Cascais, Portugal

   PDF Website

4. DimSum: A Decentralized Approach to Multi-language Semantics and Verification

   Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer

   50th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2023, Boston, United States

   Distinguished Paper Award

   PDF Website

5. Later Credits: Resourceful Reasoning for the Later Modality

   Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer

   27th ACM SIGPLAN International Conference on Functional Programming, ICFP 2022, Ljubljana, Slovenia

   PDF Website Talk

6. Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations

   Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer

   49th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2022, Philadelphia, United States

   Distinguished Paper Award

   PDF Rocq Development

7. 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

   42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, Online

   PDF Website Rocq Development Talk

8. Transfinite Step-Indexing for Termination

   Simon Spies, Neel Krishnaswami, Derek Dreyer

   48th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2021, Online

   PDF Website Talk

9. Undecidability of Higher-Order Unification Formalised in Coq

   Simon Spies, Yannick Forster

   9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, United States

   PDF Rocq Development Talk

10. Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory

    Yannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark

    8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal

    PDF Rocq Development

Dissertation

Workshops and Talks

1. Making Adequacy of Iris Satisfying

   Simon Spies

   4th Iris Workshop, Zurich, Switzerland

   Slides Rocq Demo

2. A Coq Library of Undecidable Problems

   Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, Maximilian Wuttke

   6th International Workshop on Coq for Programming Languages, CoqPL 2020, New Orleans, USA

   PDF Rocq Development