Picture of Simon Spies

Hi, I'm Simon Spies.

I am a 4th year PhD student with Derek Dreyer at the Max Planck Institute for Software Systems and Saarland Informatics Campus.

My research interests are in program semantics, formal software verification, type systems, programming language design, and logic. Lately, I have been working on transfinitely step-indexed program logics, co-inductive separation logic simulations, and automating formal verification.

I obtained my Bachelor's degree at Saarland University and my Master's degree at the University of Cambridge.

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

Publications

Conferences

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

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

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

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

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

  6. Transfinite Step-Indexing for Termination.

    Simon Spies, Neel Krishnaswami, Derek Dreyer.

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

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

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

Workshops

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