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 | 38 | 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 | 26 | 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 | 19 | 2023 |
Undecidability of higher-order unification formalised in Coq S Spies, Y Forster Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 16 | 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 | 14 | 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 | 13 | 2019 |
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 | 9 | 2023 |
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 |
Formalising the Undecidability of Higher-Order Unification S Spies, B Talk | 1 | 2018 |
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 | | 2024 |
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 |