Publications

Sort by: Date | Author | Title

Gratzer, D. (2025). A Modal Deconstruction of Löb Induction. Proceedings of the ACM on Programming Languages , 9, Article 30. https://doi.org/10.1145/3704866

Haselwarter, P. G., Li, K. H., Aguirre, A., Gregersen, S. O., Tassarotti, J. & Birkedal, L. (2025). Approximate Relational Reasoning for Higher-Order Probabilistic Programs. Proceedings of the ACM on Programming Languages , 9(POPL), 1196-1226. Article 41. https://doi.org/10.1145/3704877

Meier, W., Jensen, M., Pichon-Pharabod, J. & Spitters, B. (2025). CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq. In Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 127-139). Association for Computing Machinery. https://doi.org/10.1145/3703595.3705879

Shaik, I. & van de Pol, J. (2025). CNOT-Optimal Clifford Synthesis as SAT. In J. Berg, J. Nordstrom & J. Nordstrom (Eds.), 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025 Article 28 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.SAT.2025.28

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

Jakobsen, A. B., Clausen, A. B., van de Pol, J. & Shaik, I. (2025). Depth-Optimal Quantum Layout Synthesis as SAT. In J. Berg & J. Nordstrom (Eds.), 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025 Article 16 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.SAT.2025.16

Bhargavan, K., Buyse, M., Franceschino, L., Hansen, L. L., Kiefer, F., Schneider-Bensch, J. & Spitters, B. (2025). hax: Verifying Security-Critical Rust Software Using Multiple Provers. In J. Protzenko & A. Raad (Eds.), Verified Software. Theories, Tools and Experiments - 16th International Conference, VSTTE 2024, Revised Selected Papers (pp. 96-119). Springer. https://doi.org/10.1007/978-3-031-86695-1_7

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

Sølvsten, S. C. (2025). I/O-efficient Symbolic Model Checking. [PhD thesis, Aarhus University].

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

Li, K. H., Aguirre, A., Gregersen, S. O., Haselwarter, P. G., Tassarotti, J. & Birkedal, L. (2025). Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs. Proceedings of the ACM on Programming Languages , 9(ICFP), 276-305. https://doi.org/10.1145/3747514

Conrado, G. K., Kjelstrøm, A. H., Van De Pol, J. & Pavlogiannis, A. (2025). Program Analysis via Multiple Context Free Language Reachability. Proceedings of the ACM on Programming Languages , 9, Article 18. https://doi.org/10.1145/3704854

Sølvsten, S., Rysgaard, C. M. & van de Pol, J. (2025). Random Access on Narrow Decision Diagrams in External Memory. In T. Neele & A. Wijs (Eds.), Model Checking Software: 30th International Symposium, SPIN 2024, Luxembourg City, Luxembourg, April 8–9, 2024, Proceedings (pp. 137–145). Springer. https://doi.org/10.1007/978-3-031-66149-5_7

Mathiasen, A. A., Gondelman, L., Ducruet, L., Timany, A. & Birkedal, L. (2025). Reasoning about Weak Isolation Levels in Separation Logic. Proceedings of the ACM on Programming Languages , 9(ICFP), 306-340. https://doi.org/10.1145/3747515

Liu, Z. (2025). Separation Logic for Low-level and Realistic Programs. [PhD thesis, Aarhus University].

Stepanenko, S. & Timany, A. (2025). Solving Guarded Domain Equations in Presheaves over Ordinals and Mechanizing It. In M. Fernandez (Ed.), 10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025 Article 33 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2025.33

Sølvsten, S. & van de Pol, J. (2025). Symbolic Model Checking in External Memory. ArXiv. https://doi.org/10.48550/arXiv.2505.11229

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. https://doi.org/10.1145/3703595.3705876

Gratzer, D., Weinberger, J. & Buchholtz, U. (2025). The Yoneda embedding in simplicial type theory. In Proceedings - 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025 (pp. 127-142). IEEE. https://doi.org/10.1109/LICS65433.2025.00017

Blazy, S., Tabareau, N., Stark, K. & Timany, A. (2025). Welcome from the Chairs. In CPP '25: Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. iii-iv). Association for Computing Machinery. https://doi.org/10.1145/3703595

Gregersen, S. O., Aguirre, A., Haselwarter, P. G., Tassarotti, J. & Birkedal, L. (2024). Almost-Sure Termination by Guarded Refinement. Proceedings of the ACM on Programming Languages , 8(ICFP), 203-233. Article 243. https://doi.org/10.1145/3674632

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

Hammond, A., Liu, Z., Pérami, T., Sewell, P., Birkedal, L. & Pichon-Pharabod, J. (2024). An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic. Proceedings of the ACM on Programming Languages , 8, 604-637. Article 21. https://doi.org/10.1145/3632863

Gregersen, S. O., Aguirre, A., Haselwarter, P. G., Tassarotti, J. & Birkedal, L. (2024). Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. Proceedings of the ACM on Programming Languages , 8(POPL), Article 26. https://doi.org/10.1145/3632868

Georges, A. L., Guéneau, A., Van Strydonck, T., Timany, A., Trieu, A., Devriese, D. & Birkedal, L. (2024). Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code. Journal of the ACM, 71(1), Article 3. https://doi.org/10.1145/3623510

Aguirre, A., Haselwarter, P. G., De Medeiros, M., Li, K. H., Gregersen, S. O., Tassarotti, J. & Birkedal, L. (2024). Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. Proceedings of the ACM on Programming Languages , 8, Article 246. https://doi.org/10.1145/3674635

Jakobsen, A. B., Jørgensen, R. S. M., van de Pol, J. & Pavlogiannis, A. (2024). Fast Symbolic Computation of Bottom SCCs. In B. Finkbeiner & L. Kovács (Eds.), Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2024 (pp. 110-128). Springer. https://doi.org/10.1007/978-3-031-57256-2_6

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

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

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

Protzenko, J. & Spitters, B. (2024). Modernizing FIPS for safe languages and verified libraries. Paper presented at NIST Workshop on Formal Methods within Certification Programs (FMCP 2024), Rockville, Maryland, United States. https://www.nist.gov/system/files/documents/2024/06/11/08-ProtzenkoSpitters.pdf

Frumin, D., Timany, A. & Birkedal, L. (2024). Modular Denotational Semantics for Effects with Guarded Interaction Trees. Proceedings of the ACM on Programming Languages , 8(POPL), Article 12. https://doi.org/10.1145/3632854

Sølvsten, S. & van de Pol, J. (2024). Multi-variable Quantification of BDDs in External Memory using Nested Sweeping. ArXiv. https://doi.org/10.48550/arXiv.2408.14216

Dahlsen-Jensen, M. B., Fievet, B., Petrucci, L. & de Pol, J. V. (2024). On-The-Fly Algorithm for Reachability in Parametric Timed Games. In B. Finkbeiner & L. Kovács (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings (pp. 194-212). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-57256-2_10

Neele, T. & Pol, J. V. D. (2024). Operations on Fixpoint Equation Systems. Logical Methods in Computer Science, 20(3), 5:1-5:32. https://doi.org/10.46298/LMCS-20(3:5)2024

Shaik, I. & Pol, J. V. D. (2024). Optimal Layout-Aware CNOT Circuit Synthesis with Qubit Permutation. In U. Endriss, F. S. Melo, K. Bach, A. Bugarin-Diz, J. M. Alonso-Moral, S. Barro & F. Heintz (Eds.), ECAI 2024 - 27th European Conference on Artificial Intelligence, 19-24 October 2024, Santiago de Compostela, Spain - Including 13th Conference on Prestigious Applications of Intelligent Systems (PAIS 2024) (pp. 4207-4215). IOS Press. https://doi.org/10.3233/FAIA240993

Shaik, I. & Van de Pol, J. (2024). Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits. In S. Chakraborty & J.-H. R. Jiang (Eds.), 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024 Article 26 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.SAT.2024.26

Haselwarter, P. G., Li, K. H. E. I., Medeiros, M. D. E., Gregersen, S. O., Aguirre, A., Tassarotti, J. & Birkedal, L. (2024). Tachis: Higher-Order Separation Logic with Credits for Expected Costs. Proceedings of the ACM on Programming Languages , 8(OOPSLA2), 1189 - 1218. Article 313. https://doi.org/10.1145/3689753

Sieczkowski, F., Stepanenko, S., Sterling, J. & Birkedal, L. (2024). The Essence of Generalized Algebraic Data Types. Proceedings of the ACM on Programming Languages , 8(POPL), 695-723. https://doi.org/10.1145/3632866

Haselwarter, P. G., Hvass, B. S., Hansen, L. L., Winterhalter, T., Hriţcu, C. & Spitters, B. (2024). The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. In A. Timany, D. Traytel, B. Pientka & S. Blazy (Eds.), CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 30-44). Association for Computing Machinery. https://doi.org/10.1145/3636501.3636961

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

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

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

Pientka, B., Blazy, S., Traytel, D. & Timany, A. (2024). Welcome from the Chairs. In CPP 2024 - Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with: POPL 2024 (pp. iii-iv)

Aagaard, F. L., Sterling, J. & Birkedal, L. (2023). A denotationally-based program logic for higher-order store. Electronic Notes in Theorical Informatics and Computer Science, 3. https://doi.org/10.46298/entics.12232

Sølvsten, S. & van de Pol, J. (2023). Adiar 1.1: Zero-Suppressed Decision Diagrams in External Memory. In K. Y. Rozier & S. Chaudhuri (Eds.), NASA Formal Methods: 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings (pp. 464-471). Springer. https://doi.org/10.1007/978-3-031-33170-1_28

Gleirscher, M., van de Pol, J. & Woodcock, J. (2023). A manifesto for applicable formal methods. Software and Systems Modeling, 22(6), 1737-1749. https://doi.org/10.1007/s10270-023-01124-2

Larsen, C. A., Schmidt, S. M., Steensgaard, J., Jakobsen, A. B., Pol, J. V. D. & Pavlogiannis, A. (2023). A Truly Symbolic Linear-Time Algorithm for SCC Decomposition. In S. Sankaranarayanan & N. Sharygina (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part II (pp. 353-371). Springer. https://doi.org/10.1007/978-3-031-30820-8_22

Shaik, I. & van de Pol, J. (2023). Concise QBF Encodings for Games on a Grid (extended version). https://doi.org/10.48550/arXiv.2303.16949

Madsen, M., Van De Pol, J. & Henriksen, T. (2023). Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems. Proceedings of the ACM on Programming Languages , 7(OOPSLA2), 516–543. Article 240. https://doi.org/10.1145/3622816

Displaying results 1 to 50 out of 355

Revised 01.09.2025

Sofia Hedegaard Rasmussen