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 | 41 | 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 | 19 | 2021 |

Undecidability of higher-order unification formalised in Coq S Spies, Y Forster Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 12 | 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 | 10 | 2019 |

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 | 9 | 2022 |

Transfinite Step-Indexing for Termination S Spies, N Krishnaswami, D Dreyer | 3 | 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 | 2 | 2022 |

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 |