Publications

Sort by: Date | Author | Title

Rijke, E., Shulman, M. & Spitters, B. (2017, Jun 27). Modalities in homotopy type theory. https://arxiv.org/abs/1706.07526

Rijke, E., Shulman, M. & Spitters, B. (2020). Modalities in homotopy type theory. Logical Methods in Computer Science, 16(1), 2:1-2:79.

Gratzer, D., Cavallo, E., Kavvos, G. A., Guatto, A. & Birkedal, L. (2022). Modalities and Parametric Adjoints. ACM Transactions on Computational Logic, 23(3), Article 18. https://doi.org/10.1145/3514241

Birkedal, L., Clouston, R., Mannaa, B., Ejlers Møgelberg, R., Pitts, A. M. & Spitters, B. (2020). Modal dependent type theory and dependent right adjoints. Mathematical Structures in Computer Science, 30(2), 118-138. https://doi.org/10.1017/S0960129519000197

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

André, É., Bloemen, V., Petrucci, L. & Pol, J. V. D. (2019). Minimal-Time Synthesis for Parametric Timed Automata. In L. Zhang & T. Vojnar (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings (Vol. II, pp. 211-228). Springer. https://doi.org/10.1007/978-3-030-17465-1_12

Nelson, B., Pagnin, E. & Askarov, A. (2024). Metadata Privacy Beyond Tunneling for Instant Messaging. In Proceedings - 9th IEEE European Symposium on Security and Privacy, EuroS&P 2024 (pp. 697-723). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/EuroSP60621.2024.00044

Guéneau, A., Hostert, J., Spies, S., Sammler, M., Birkedal, L. & Dreyer, D. (2023). Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. Proceedings of the ACM on Programming Languages , 7(OOPSLA2), 716-744. Article 247. https://doi.org/10.1145/3622823

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

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

Gregersen, S. O., Bay, J., Timany, A. & Birkedal, L. (2021). Mechanized logical relations for termination-insensitive noninterference. Proceedings of the ACM on Programming Languages , 5(POPL), Article 10. https://doi.org/10.1145/3434291

Birkedal, L., Damgaard, T. C., Glenstrup, A. J. & Milner, R. (2007). Matching of Bigraphs. Electronic Notes in Theoretical Computer Science, 175(4 SPEC. ISS.), 3-19. https://doi.org/10.1016/j.entcs.2007.04.013

Dreyer, D., Ahmed, A. & Birkedal, L. (2009). Logical Step-Indexed Logical Relations. In Proceedings of the Twenty-Fourth Annual IEEE Symposium on Logic in Computer Science, LICS 2009, Los Angeles, CA, USA IEEE Computer Society Press.

Dreyer, D., Ahmed, A. & Birkedal, L. (2011). Logical Step-Indexed Logical Relations. Logical Methods in Computer Science, 7(2:16). https://doi.org/10.2168/LMCS-7(2:16)2011

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.

Birkedal, L., Torp-Smith, N. & Reynolds, J. C. (2004). Local reasoning about a copying garbage collector. SIGPLAN Notices, 39(1), 220-231. http://www.scopus.com/inward/record.url?scp=1442263140&partnerID=8YFLogxK

Awodey, S., Birkedal, L. & Scott, D. S. (1999). Local realizability toposes and a modal logic for computability - (Extended Abstract). Electronic Notes in Theoretical Computer Science, 23(1), 13-26. https://doi.org/10.1016/S1571-0661(04)00101-X

Awodey, S., Birkedal, L. & Scott, D. S. (2002). Local realizability toposes and a modal logic for computability. Mathematical Structures in Computer Science, 12(3), 319-334. https://doi.org/10.1017/S0960129502003675

Birkedal, L., Møgelberg, R. E. & Lerc Petersen, R. (2006). Linear Abadi and Plotkin Logic. Logical Methods in Computer Science, 2(5), Article 2. https://doi.org/10.2168/LMCS-2(5:2)2006

Møgelberg, R. E., Birkedal, L. & Petersen, R. L. (2006). Linear Abadi & Plotkin Logic. Logical Methods in Computer Science, 2/5. https://doi.org/10.2168/LMCS-2(5:2)2006

Birkedal, L., Petersen, R. L., Møgelberg, R. E. & Warming, C. (2006). LILY Operational Semantics and Models of Linear Abadi-Plotkin Logic. IT University of Copenhagen. I T University. Technical Report Series No. TR-2006-83

Georges, A. L., Trieu, A. & Birkedal, L. (2022). Le temps des cerises: Efficient temporal stack safety on capability machines using directed capabilities. Proceedings of the ACM on Programming Languages , 6(OOPSLA1), Article 74. https://doi.org/10.1145/3527318

Abel, A., Cockx, J., Devriese, D., Timany, A. & Wadler, P. (2020). Leibniz equality is isomorphic to Martin-Löf identity, parametrically. Journal of Functional Programming, 30, Article e17. https://doi.org/10.1017/S0956796820000155

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

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

André, É., Arias, J., Petrucci, L. & Pol, J. V. D. (2021). Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata. In J. F. Groote & K. G. Larsen (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021: 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings, Part I (pp. 311-329). Springer. https://doi.org/10.1007/978-3-030-72016-2_17

Sammler, M., Hammond, A., Lepigre, R., Campbell, B., Pichon-Pharabod, J., Dreyer, D., Garg, D. & Sewell, P. (2022). Islaris: verification of machine code against authoritative ISA semantics. In R. Jhala & I. Dillig (Eds.), PLDI 2022 - Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 825-840). Association for Computing Machinery. https://doi.org/10.1145/3519939.3523434

Bizjak, A., Gratzer, D., Krebbers, R. & Birkedal, L. (2019). Iron: managing obligations in higher-order concurrent separation logic. Proceedings of the ACM on Programming Languages , 3(POPL), 1-30. Article 65. https://doi.org/10.1145/3290378

Rao, X., Georges, A. L., Legoupil, M., Watt, C., Pichon-Pharabod, J., Gardner, P. & Birkedal, L. (2023). Iris-Wasm: Robust and Modular Verification of WebAssembly Programs. Proceedings of the ACM on Programming Languages , 7, Article 151. https://doi.org/10.1145/3591265

Legoupil, M., Rousseau, J., Georges, A. L., Pichon-Pharabod, J. & Birkedal, L. (2024). Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly. Proceedings of the ACM on Programming Languages , 8(OOPSLA2), Article 282. https://doi.org/10.1145/3689722

JUNG, RALF., KREBBERS, ROBBERT., JOURDAN, JACQUES.-HENRI., BIZJAK, ALEŠ., BIRKEDAL, LARS. & DREYER, DEREK. (2018). Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28, 1-73. Article e20. https://doi.org/10.1017/S0956796818000151

Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L. & Dreyer, D. (2015). Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In S. Rajamani (Ed.), Conference Record of the Annual ACM Symposium on Principles of Programming Languages (pp. 637-650). Association for Computing Machinery. https://doi.org/10.1145/2676726.2676980

Licata, D. R., Orton, I., Pitts, A. M. & Spitters, B. (2018, Jul 1). Internal Universes in Models of Homotopy Type Theory. arxiv.org. https://arxiv.org/abs/1801.07664

Krebbers, R., Timany, A. & Birkedal, L. (2017). Interactive proofs in higher-order concurrent separation logic. In A. D. Gordon & G. Castagna (Eds.), Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 (pp. 205-217). Association for Computing Machinery. https://doi.org/10.1145/3009837.3009855

Birkedal, L. & Mogelberg, R. E. (2013). Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes. Annual Symposium on Logic in Computer Science, 213-222. https://doi.org/10.1109/LICS.2013.27

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

Shaik, I., Mayer-Eichberger, V., van de Pol, J. & Saffidine, A. (2023). Implicit State and Goals in QBF Encodings for Positional Games (extended version). https://doi.org/10.48550/arXiv.2301.07345

Shaik, I., Mayer-Eichberger, V., van de Pol, J. & Saffidine, A. (2024). Implicit QBF Encodings for Positional Games. In M. Hartisch, C.-H. Hsueh & J. Schaeffer (Eds.), Advances in Computer Games - 18th International Conference, ACG 2023, Revised Selected Papers (pp. 133-145). Springer. https://doi.org/10.1007/978-3-031-54968-7_12

Gratzer, D., Sterling, J. & Birkedal, L. (2019). Implementing a modal dependent type theory. Proceedings of the ACM on Programming Languages , 3(ICFP), 1-29. Article 107. https://doi.org/10.1145/3341711

Gratzer, D., Møller, M. A. & Birkedal, L. (2025). Idempotent Resources in Separation Logic: The Heart of core in Iris. In P. A. Abdulla & D. Kesner (Eds.), Foundations of Software Science and Computation Structures - 28th International Conference, FoSSaCS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software: ETAPS 2025, Proceedings (pp. 45-66). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-90897-2_3

Askarov, A., Chong, S. & Mantel, H. A. (2015). Hybrid Monitors for Concurrent Noninterference. In L. Viganò (Ed.), 28th IEEE Computer Security Foundations Symposium CSF 2015 : Proceedings (pp. 137 - 151). IEEE Computer Society Press. https://doi.org/10.1109/CSF.2015.17

Rijke, E. & Spitters, B. (2016). Homotopy type theory and the formalization of mathematics. Nieuw Archief voor Wiskunde , 5/17(3), 159 - 164. http://www.cs.au.dk/~spitters/naw5-2016-17-3-159.pdf

Nanevski, A., Morrisett, J. G. & Birkedal, L. (2008). Hoare type theory, polymorphism and separation. Journal of Functional Programming, 18(5-6), 865-911.

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

Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Katsumata, S. Y. & Sato, T. (2021). Higher-order probabilistic adversarial computations: categorical semantics and program logics. Proceedings of the ACM on Programming Languages , 5(ICFP), Article 93. https://doi.org/10.1145/3473598

Jung, R., Krebbers, R., Birkedal, L. & Dreyer, D. (2016). Higher-order ghost state. In E. Sumii (Ed.), ICFP 2016 Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (pp. 256-269). Association for Computing Machinery. https://doi.org/10.1145/2951913.2951943

Birkedal, L., Bundgaard, M., Debois, S., Grohmann, D. & Hildebrandt, T. (2009). Higher-order contexts via games and the Int-construction. (pp. 32). IT University of Copenhagen. I T University. Technical Report Series Vol. TR-2009-117

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

Hvass, B. S., Aranha, D. F. & Spitters, B. (2020). High-assurance field inversion for pairing-friendly primes. Abstract from The Coq Workshop 2020. https://coq-workshop.gitlab.io/2020/abstracts/Coq2020_04-02-primes.pdf

Displaying results 151 to 200 out of 345

Revised 17.04.2023

Sofia Hedegaard Rasmussen