Follow
Simon Spies
Simon Spies
Verified email at mpi-sws.org - Homepage
Title
Cited by
Cited by
Year
A Coq library of undecidable problems
Y Forster, D Larchey-Wendling, A Dudenhefner, E Heiter, D Kirst, F Kunze, ...
CoqPL 2020 The Sixth International Workshop on Coq for Programming Languages, 2020
412020
Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic
S Spies, L Gäher, D Gratzer, J Tassarotti, R Krebbers, D Dreyer, ...
Proceedings of the 42nd ACM SIGPLAN International Conference on Programming …, 2021
192021
Undecidability of higher-order unification formalised in Coq
S Spies, Y Forster
Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020
122020
Call-by-push-value in Coq: operational, equational, and denotational theory
Y Forster, S Schäfer, S Spies, K Stark
Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019
102019
Simuliris: a separation logic framework for verifying concurrent program optimizations
L Gäher, M Sammler, S Spies, R Jung, HH Dang, R Krebbers, J Kang, ...
Proceedings of the ACM on Programming Languages 6 (POPL), 1-31, 2022
92022
Transfinite Step-Indexing for Termination
S Spies, N Krishnaswami, D Dreyer
32020
Later credits: resourceful reasoning for the later modality
S Spies, L Gäher, J Tassarotti, R Jung, R Krebbers, L Birkedal, D Dreyer
Proceedings of the ACM on Programming Languages 6 (ICFP), 283-311, 2022
22022
Semantics of Type Systems Lecture Notes
D Dreyer, R Jung, JO Kaiser, HH Dang, D Swasey, J Menz, L Gäher, ...
22022
Formalising the Undecidability of Higher-Order Unification
S Spies, B Talk
12018
Simuliris: A Separation Logic Framework for Verifying rent Program Optimizations
L Gähler, M Sammler, S Spies, R Jung, HH Dang, RJ Krebbers, J Kang, ...
2022
The system can't perform the operation now. Try again later.
Articles 1–10