| 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 | 45 | 2020 |
| 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 | 29 | 2021 |
| 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 | 18 | 2022 |
| Undecidability of higher-order unification formalised in Coq S Spies, Y Forster Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 14 | 2020 |
| 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 | 12 | 2019 |
| DimSum: A Decentralized Approach to Multi-language Semantics and Verification M Sammler, S Spies, Y Song, E D'Osualdo, R Krebbers, D Garg, D Dreyer Proceedings of the ACM on Programming Languages 7 (POPL), 775-805, 2023 | 6 | 2023 |
| 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 | 5 | 2022 |
| Melocoton: A Program Logic for Verified Interoperability Between OCaml and C A Guéneau, J HOSTERT, S SPIES, M SAMMLER, L BIRKEDAL, ... | 3 | 2023 |
| Transfinite Step-Indexing for Termination S Spies, N Krishnaswami, D Dreyer | 3 | 2020 |
| Semantics of Type Systems Lecture Notes D Dreyer, R Jung, JO Kaiser, HH Dang, D Swasey, J Menz, L Gäher, ... | 2 | 2022 |
| Formalising the Undecidability of Higher-Order Unification S Spies, B Talk | 1 | 2018 |
| 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 |
