Publications

Sort by: Date | Author | Title

Wimmer, S., Herbreteau, F. & van de Pol, J. (2020). Certifying Emptiness of Timed Büchi Automata. In N. Bertrand & N. Jansen (Eds.), Formal Modeling and Analysis of Timed Systems : 18th International Conference, FORMATS 2020 (pp. 58-75). Springer. https://doi.org/10.1007/978-3-030-57628-8_4

Vindum, S. F. & Birkedal, L. (2021). Contextual refinement of the Michael-Scott queue (proof pearl). In C. Hriţcu & A. Popescu (Eds.), CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 76-90). Association for Computing Machinery. https://doi.org/10.1145/3437992.3439930

Vindum, S. F., Frumin, D. & Birkedal, L. (2022). Mechanized Verification of a Fine-Grained Concurrent Queue from Meta s Folly Library. In A. Popescu & S. Zdancewic (Eds.), CPP 2022 : Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022 (pp. 100-115). Association for Computing Machinery. https://doi.org/10.1145/3497775.3503689

Vindum, S. F. & Birkedal, L. (2023). Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory. Proceedings of the ACM on Programming Languages , 7(OOPSLA2), 632-657. Article 244. https://doi.org/10.1145/3622820

Vindum, S. F., Georges, A. L. & Birkedal, L. (2025). The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic. In K. Stark, A. Timany, S. Blazy & N. Tabareau (Eds.), Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with: POPL 2025 (pp. 83-97). Association for Computing Machinery, Inc.. https://doi.org/10.1145/3703595.3705876

Varming, C. & Birkedal, L. (2008). Higher-Order Separation Logic in Isabelle/HOLCF. Electronic Notes in Theoretical Computer Science, 218, 371-389. https://doi.org/10.1016/j.entcs.2008.10.022

Van Der Berg, F. I. & Van De Pol, J. (2019). Concurrent chaining hash maps for software model checking. In C. Barrett & J. Yang (Eds.), Proceedings of the 19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019 (pp. 46-54). Article 8894279 IEEE. https://doi.org/10.23919/FMCAD.2019.8894279

van de Pol, J. (2019). Concurrent algorithms and data structures for model checking. In W. Fokkink & R. van Glabbeek (Eds.), 30th International Conference on Concurrency Theory, CONCUR 2019 Article 4 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CONCUR.2019.4

van de Pol, J. (2022). Exploring a Parallel SCC Algorithm: Using TLA ⁺ and the TLC Model Checker. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings (pp. 535-555). Springer. https://doi.org/10.1007/978-3-031-19849-6_30

van de Pol, J. & Petrucci, L. (2021). On Completeness of Liveness Synthesis for Parametric Timed Automata (Extended Abstract). In M. Roggenbach (Ed.), Recent Trends in Algebraic Development Techniques - 25th International Workshop, WADT 2020, Revised Selected Papers (pp. 3-10). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-73785-6_1

Turon, A., Dreyer , D. & Birkedal, L. (2013). Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In G. Morrisett & T. Uustalu (Eds.), Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP '13 (pp. 377-390 ). Association for Computing Machinery. https://doi.org/10.1145/2500365.2500600

Turon, A. J., Thamsborg, J., Ahmed, A., Birkedal, L. & Dreyer, D. (2013). Logical relations for fine-grained concurrency. In POPL '13 Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (pp. 343-356). Association for Computing Machinery. https://doi.org/10.1145/2429069.2429111

Torp-Smith, N., Birkedal, L. & Reynolds, J. C. (2008). Local Reasoning about a Copying Garbage Collector. A C M Transactions on Programming Languages and Systems, 30(4), 24-81.

Tofte, M. & Birkedal, L. (1998). A Region Inference Algorithm. A C M Transactions on Programming Languages and Systems, 20(4), 724-767. http://www.scopus.com/inward/record.url?scp=0032108162&partnerID=8YFLogxK

Tofte, M., Birkedal, L., Elsman, M. & Hallenberg, N. (2004). A retrospective on Region-based Memory Management. Higher-Order and Symbolic Computation, 17(3), 245-265. https://doi.org/10.1023/B:LISP.0000029446.78563.a4

Tofte, M. & Birkedal, L. (2000). Unification and polymorphism in region inference: essays in honour of Robin Milner. In G. Plotkin , C. Stirling & M. Tofte (Eds.), Proof, language, and interaction (pp. 389-423 ). MIT Press. http://dl.acm.org/citation.cfm?id=345868.345907&coll=DL&dl=GUIDE&CFID=560593603&CFTOKEN=90733199

Timany, A., Stefanesco, L., Krogh-Jespersen, M. & Birkedal, L. (2018). A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST. In Proceedings of the ACM on Programming Languages (Vol. 2, pp. 64:00-64:28). Association for Computing Machinery. https://doi.org/10.1145/3158152

Timany, A. & Birkedal, L. (2019). Mechanized relational verification of concurrent programs with continuations. Proceedings of the ACM on Programming Languages , 3(ICFP), 1-28. Article 105. https://doi.org/10.1145/3341709

Timany, A. & Sozeau, M. (2018). Cumulative inductive types in coq. In H. Kirchner (Ed.), 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018 Article 29 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2018.29

Timany, A. & Birkedal, L. (2021). Reasoning about monotonicity in separation logic. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’21) (pp. 91-104). Association for Computing Machinery. https://doi.org/10.1145/3437992.3439931

Timany, A., Guéneau, A. & Birkedal, L. (2024). The Logical Essence of Well-Bracketed Control Flow. Proceedings of the ACM on Programming Languages , 8(POPL), 575-603. https://doi.org/10.1145/3632862

Timany, A., Gregersen, S. O., Stefanesco, L., Hinrichsen, J. K., Gondelman, L., Nieto, A. & Birkedal, L. (2024). Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement. Proceedings of the ACM on Programming Languages , 8, Article 9. https://doi.org/10.1145/3632851

Timany, A., Krebbers, R., Dreyer, D. & Birkedal, L. (2024). A Logical Approach to Type Soundness. Journal of the ACM, 71(6), Article 40. https://doi.org/10.1145/3676954

Thomsen, S. E. & Spitters, B. (2020). Formalizing Nakamoto-Style Proof of Stake.

Thomsen, S. E. & Spitters, B. (2021). Formalizing Nakamoto-Style Proof of Stake. In Proceedings - 2021 IEEE 34th Computer Security Foundations Symposium, CSF 2021 IEEE. https://doi.org/10.1109/CSF51468.2021.00042

Thamsborg, J. J. & Birkedal, L. (2011). A Kripke Logical Relation for Effect-Based Program Transformations. In ICFP 11. Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (pp. 445-456). Association for Computing Machinery. https://doi.org/10.1145/2034574.2034831

Thamsborg, J. J., Birkedal, L. & Yang, H. (2012). Two for the Price of One: Lifting Separation Logic Assertions. Logical Methods in Computer Science, 8(3).

Svendsen, K. & Birkedal, L. (2014). Impredicative concurrent abstract predicates. In Z. Shao (Ed.), Programming Languages and Systems: 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings (pp. 149-168 ). Springer. https://doi.org/10.1007/978-3-642-54833-8_9

Svendsen, K., Birkedal, L. & Nanevski, A. (2011). Partiality, State, and Dependent Types. In Proceedings of Typed LAmbda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011 (Vol. LNCS 6690, pp. 198-212). Springer.

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Higher-order Concurrent Abstract Predicates.

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Verification of the Joins Library in Higher-Order Separation Logic. http://www.itu.dk/people/kasv/joins-tr.pdf

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Modular Reasoning about Separation of Concurrent Data Structures. In M. Felleisen & P. Gardner (Eds.), Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings (pp. 169-188 ). Springer. https://doi.org/10.1007/978-3-642-37036-6_11

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Joins: A case study in modular specification of a concurrent reentrant higher-order library. In G. Castagna (Ed.), 27th European Conference on Object-Oriented Programming, ECOOP 2013; Montpellier; France (pp. 327-351). Springer. https://doi.org/10.1007/978-3-642-39038-8_14

Svendsen, K., Birkedal, L. & Parkinson, M. (2010). Verifying generics and delegates. In ECOOP 2010 – Object-Oriented Programming: 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings (pp. 175-199). Springer. https://doi.org/10.1007/978-3-642-14107-2_9

Svendsen, K., Buisse, A. & Birkedal, L. (2008). Verifying design patterns in Hoare type theory. IT University of Copenhagen. I T University. Technical Report Series No. TR-2008-112

Svendsen, K., Sieczkowski, F. & Birkedal, L. (2016). Transfinite step-indexing: Decoupling concrete and logical steps. In P. Thiemann (Ed.), Programming Languages and Systems (Vol. 9632, pp. 727-751). Springer VS. https://doi.org/10.1007/978-3-662-49498-1_28

Strydonck, T. V., Georges, A. L., Guéneau, A., Trieu, A., Timany, A., Piessens, F., Birkedal, L. & Devriese, D. (2022). Proving full-system security properties under multiple attacker models on capability machines. In Proceedings - 2022 IEEE 35th Computer Security Foundations Symposium, CSF 2022 (pp. 80-95). IEEE. https://doi.org/10.1109/CSF54842.2022.9919645

Sterling, J., Angiuli, C. & Gratzer, D. (2019). Cubical syntax for reflection-free extensional equality. In H. Geuvers (Ed.), 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019 Article 31 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2019.31

Sterling, J., Angiuli, C. & Gratzer, D. (2022). A cubical language for bishop sets. Logical Methods in Computer Science, 18(1), 43:1-43:80. https://doi.org/10.46298/LMCS-18(1:43)2022

Sterling, J., Gratzer, D. & Birkedal, L. (2024). Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. In A. Murano & A. Silva (Eds.), 32nd EACSL Annual Conference on Computer Science Logic, CSL 2024 Article 47 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2024.47

Stepanenko, S., Nardino, E., Frumin, D., Timany, A. & Birkedal, L. (2025). Context-Dependent Effects in Guarded Interaction Trees. In V. Vafeiadis (Ed.), Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings (Vol. Part II, pp. 286-313). Springer. https://doi.org/10.1007/978-3-031-91121-7_12

Stassen, P. J. A., Gratzer, D. & Birkedal, L. (2023). mitten: A Flexible Multimodal Proof Assistant. In D. Kesner & P.-M. Pedrot (Eds.), 28th International Conference on Types for Proofs and Programs Article 6 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.TYPES.2022.6

Stassen, P., Møgelberg, R. E., Zwart, M. A., Aguirre, A. & Birkedal, L. (2025). Modelling Recursion and Probabilistic Choice in Guarded Type Theory. Proceedings of the ACM on Programming Languages , 9(POPL), 1417-1445. Article 48. https://doi.org/10.1145/3704884

Spitters, B. (2015). Cubical sets as a classifying topos. Abstract from 21st International Conference on Types for Proofs and Programs, , Tallinn, Estonia.

Spitters, B. (2016, Oct 17). Cubical sets and the topological topos. https://arxiv.org/pdf/1610.05270v1.pdf

Spitters, B., Vickers, S. & Wolters, S. (2014). Gelfand spectra in Grothendieck toposes using geometric mathematics. Electronic Proceedings in Theoretical Computer Science, EPTCS, 158, 77-107. https://doi.org/10.4204/EPTCS.158.7

Spitters, B. (2012). The Space of Measurement Outcomes as a Spectral Invariant for Non-Commutative Algebras. Foundations of Physics, 42(7), 896-908. https://doi.org/10.1007/s10701-011-9619-3

Spies, S., Gäher, L., Gratzer, D., Tassarotti, J., Krebbers, R., Dreyer, D. & Birkedal, L. (2021). Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic. In S. N. Freund & E. Yahav (Eds.), PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 80-95). Association for Computing Machinery. https://doi.org/10.1145/3453483.3454031

Spies, S., Gäher, L., Tassarotti, J., Jung, R., Krebbers, R., Birkedal, L. & Dreyer, D. (2022). Later credits: resourceful reasoning for the later modality. Proceedings of the ACM on Programming Languages , 6(ICFP), Article 100. https://doi.org/10.1145/3547631

Sørensen, J. A., Kristoffersen, K. J., Cervera, A., Schiøtz, M., Lynge, T., Safar, Z. & Birkedal, L. (2004). An infrastructure for context dependent mobile multimedia communication. In 2004 IEEE 6th Workshop on Multimedia Signal Processing (pp. 462-464). IEEE Press. https://doi.org/10.1109/MMSP.2004.1436595

Displaying results 1 to 50 out of 345

Revised 17.04.2023

Sofia Hedegaard Rasmussen