Simon Spies

According to our database, Simon Spies authored at least 8 papers between 2019 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

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., October, 2023

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

Proc. ACM Program. Lang., January, 2023

2022

Later credits: resourceful reasoning for the later modality.

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

Proc. ACM Program. Lang., 2022

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

Proc. ACM Program. Lang., 2022

2021

Transfinite step-indexing for termination.

Simon Spies, Neel Krishnaswami, Derek Dreyer

Proc. ACM Program. Lang., 2021

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

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

2020

Undecidability of higher-order unification formalised in Coq.

Simon Spies, Yannick Forster

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2019

Call-by-push-value in coq: operational, equational, and denotational theory.

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

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019