| 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 | 48 | 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 | 45 | 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 | 33 | 2022 |
| 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 | 24 | 2023 |
| Melocoton: A program logic for verified interoperability between ocaml and c A Guéneau, J Hostert, S Spies, M Sammler, L Birkedal, D Dreyer Proceedings of the ACM on Programming Languages 7 (OOPSLA2), 716-744, 2023 | 20 | 2023 |
| Undecidability of higher-order unification formalised in Coq S Spies, Y Forster Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 18 | 2020 |
| 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 | 17 | 2022 |
| 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 | 16 | 2019 |
| Transfinite Step-Indexing for Termination S Spies, N Krishnaswami, D Dreyer | 8 | 2020 |
| Semantics of Type Systems Lecture Notes D Dreyer, S Spies, L Gäher, R Jung, JO Kaiser, HH Dang, D Swasey, ... July, 2022 | 3 | 2022 |
| Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq S Spies, L Gäher, M Sammler, D Dreyer Proceedings of the ACM on Programming Languages 8 (PLDI), 889-913, 2024 | 1 | 2024 |
| 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 |
Derek DreyerMax Planck Institute for Software Systems (MPI-SWS), Saarland Informatics CampusVerified email at mpi-sws.org