Publications

Sort by: Date | Author | Title

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

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

Dreyer, D., Neis, G. & Birkedal, L. (2010). The impact of higher-order state and control effects on local relational reasoning. In S. Weirich & P. Hudak (Eds.), Proceedings of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010 (pp. 143-156). Association for Computing Machinery. https://doi.org/10.1145/1863543.1863566

Dreyer, D., Neis, G. & Birkedal, L. (2012). The impact of higher-order state and control effects on local relational reasoning. Journal of Functional Programming, 22(4-5 special issue), 477-528. https://doi.org/10.1017/S0956796812000287

Bauer, A., Gross, J., Lumsdaine, P. L., Shulman, M., Sozeau, M. & Spitters, B. (2017). The HoTT Library: A Formalization of Homotopy Type Theory in Coq. In Y. Bertot & V. Vafeiadis (Eds.), CPP 2017 - Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2017: CPP 2017 (pp. 164-172). Association for Computing Machinery. https://doi.org/10.1145/3018610.3018615

Bauer, A., Gross, J., Lumsdaine, P. L., Shulman, M., Sozeau, M. & Spitters, B. (2016). The HoTT Library: A formalization of homotopy type theory in Coq. http://arxiv.org/abs/1610.04591

Clouston, R., Bizjak, A., Grathwohl, H. B. & Birkedal, L. (2016). The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Logical Methods in Computer Science, 12(3), 1 - 39. https://doi.org/10.2168/LMCS-12(3:7)2016

Jung, R., Lepigre, R., Parthasarathy, G., Rapoport, M., Timany, A., Dreyer, D. & Jacobs, B. (2020). The future is ours: prophecy variables in separation logic. Proceedings of the ACM on Programming Languages , 4(POPL), Article 45. https://doi.org/10.1145/3371113

Pavlogiannis, A. (2020). The Fine-Grained Complexity of Andersen's Pointer Analysis. ArXiv. https://arxiv.org/abs/2006.01491

Mathiasen, A. A. & Pavlogiannis, A. (2021). The Fine-Grained and Parallel Complexity of Andersen’s Pointer Analysis. Proceedings of the ACM on Programming Languages , 5(POPL), Article 34. https://doi.org/10.1145/3434315

Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D. & Birkedal, L. (2017). The Essence of Higher-Order Concurrent Separation Logic. In H. Yang (Ed.), Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings (pp. 696-723). Springer VS. https://doi.org/10.1007/978-3-662-54434-1_26

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

Klarlund, N., Møller, A. & Schwartzbach, M. I. (2002). The DSD Schema Language. Automated Software Engineering, 9(3), 285-319. https://doi.org/10.1023/A:1016376608070

Møller, A. & Schwartzbach, M. I. (2005). The Design Space of Type Checkers for XML Transformation Languages. In Database Theory - ICDT 2005: 10th International Conference, Edinburgh, UK, January 5-7, 2005. Proceedings (pp. 17-36). Springer. https://doi.org/10.1007/978-3-540-30570-5_2

Kjelstrom, A. H. & Pavlogiannis, A. (2022). The Decidability and Complexity of Interleaved Bidirected Dyck Reachability. Proceedings of the ACM on Programming Languages , 6(POPL), Article 12. https://doi.org/10.1145/3498673

Shi, Z., Møldrup, L., Mathur, U. & Pavlogiannis, A. (2026). The Complexity of Testing Message-Passing Concurrency. Proceedings of the ACM on Programming Languages , 10, 1-32. https://doi.org/10.1145/3776643

Mathur, U., Pavlogiannis, A. & Viswanathan, M. (2020). The Complexity of Dynamic Data Race Prediction. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 (pp. 713–727). Article 3394783 Association for Computing Machinery. https://doi.org/10.1145/3373718.3394783

Birkedal, L., Støvring, K. & Thamsborg, J. J. (2010). The category-theoretic solution of recursive metric-space equations. Theoretical Computer Science, 411(47), 4102-4122.

Feldthaus, A. & Møller, A. (2009). The Big Manual for the Java String Analyzer: Latest release: version 2.1-1, November 30, 2009. http://www.brics.dk/JSA/

Garavel, H., ter Beek, M. H. & van de Pol, J. (2020). The 2020 Expert Survey on Formal Methods. In M. H. ter Beek & D. Nickovic (Eds.), Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Proceedings: FMICS 2020, Vienna, Austria, September 2-3, 2020, Proceedings (pp. 3-69). Springer. https://doi.org/10.1007/978-3-030-58298-2_1

Møller, A. (2018). Technical Perspective: WebAssembly: A Quiet Revolution of the Web. Communications of the A C M, 61(12), 106-106. https://doi.org/10.1145/3282508

Madsen, M., Zarifi, R. & Lhoták, O. (2018). Tail Call Elimination and Data Representation for Functional Languages on the Java Virtual Machine. In J. Xue & C. Dubach (Eds.), CC 2018 - Proceedings of the 27th International Conference on Compiler Construction, Co-located with CGO 2018 (pp. 139-150). Association for Computing Machinery. https://doi.org/10.1145/3178372.3179499

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

Adamsen, C. Q., Møller, A. & Mezzetti, G. (2015). Systematic Execution of Android Test Suites in Adverse Conditions. In Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA '15 (pp. 83-93 ). Association for Computing Machinery. https://doi.org/10.1145/2771783.2771786

Billes, M., Møller, A. & Pradel, M. (2017). Systematic black-box analysis of collaborative web applications. In PLDI 2017 - Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (Vol. Part F128414, pp. 171-184). Association for Computing Machinery. https://doi.org/10.1145/3062341.3062364

Andreasen, E. S., Møller, A. & Nielsen, B. B. (2017). Systematic Approaches for Increasing Soundness and Precision of Static Analyzers. In K. Ali & C. Cifuentes (Eds.), SOAP 2017 - Proceedings of the 6th ACM SIGPLAN International Workshop on State of the Art in Program Analysis, co-located with PLDI 2017 (pp. 31-36). Association for Computing Machinery. https://doi.org/10.1145/3088515.3088521

Bidlingmaier, M. E., Faissole, F. & Spitters, B. (2019). Synthetic topology in Homotopy Type Theory for probabilistic programming. ArXiv.

Bidlingmaier, M. E., Faissole, F. & Spitters, B. (2021). Synthetic topology in Homotopy Type Theory for probabilistic programming. Mathematical Structures in Computer Science, 31(10), 1301-1329. https://doi.org/10.1017/S0960129521000165

Møgelberg, R. E., Birkedal, L. & Rosolini, G. (2008). Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic. Annals of Pure and Applied Logic, 155(2), 115-133.

Møgelberg, R. E., Birkedal, L. & Rosolini, G. (2006). Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic. Electronic Notes in Theoretical Computer Science, 155(1 SPEC. ISS.), 219-245. https://doi.org/10.1016/j.entcs.2005.11.058

Hansen, S. T., Gomes, C., Larsen, P. G. & Van De Pol, J. (2021). Synthesizing Co-Simulation Algorithms with Step Negotiation and Algebraic Loop Handling. In C. R. Martin, M. J. Blas & A. I. Psijas (Eds.), 2021 Annual Modeling and Simulation Conference (ANNSIM) (pp. 62-73). IEEE. https://doi.org/10.23919/ANNSIM52504.2021.9552073

Gratzer, D. (2023). Syntax and semantics of modal type theory. [PhD dissertation, Aarhus University]. Aarhus University.

Pichon-Pharabod, J. (2025). Synchronous Programming for Kids: A Manifesto. In S. Chiba, C. N. Klokmose & C. Gordon (Eds.), Onward! 2025 - Proceedings of the 2025 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Co-located with SPLASH 2025 (pp. 1-12). Association for Computing Machinery. https://doi.org/10.1145/3759429.3762617

Pol, J. V. D. & Meijer, J. (2019). Synchronous or Alternating? LTL Black-Box Checking of Mealy Machines by Combining the LearnLib and LTSmin. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): The What, the How, and the Why Not? (pp. 417-430). Springer. https://doi.org/10.1007/978-3-030-22348-9_24

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

Mortensen, K. O., Skitsas, K., Christensen, E. M., Talebi, M. S., Pavlogiannis, A., Mottin, D. & Karras, P. (2025). SwiftVI: Time-Efficient Planning and Learning with MDPs. In M. Zaharia, G. Joshi & Y. Lin (Eds.), Proceedings of Machine Learning and Systems (Vol. 7). MLSys. https://proceedings.mlsys.org/paper_files/paper/2025/file/0f8426558905746fc38da5e335700aec-Paper-Conference.pdf

Madsen, M. & Andreasen, E. (2014). String Analysis for Dynamic Field Access. In A. Cohen (Ed.), Compiler Construction: 23rd International Conference, CC 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. 197-217). Springer. https://doi.org/10.1007/978-3-642-54807-9_12

Skorstensgaard, L., Devriese, D. & Birkedal, L. (2021). StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities. Journal of Functional Programming, 31, Article e9. https://doi.org/10.1017/S095679682100006X

Skorstengaard, L., Devriese, D. & Birkedal, L. (2019). StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities. Proceedings of the ACM on Programming Languages , 3(POPL), Article 19. https://doi.org/10.1145/3290332

Birkedal, L., Bizjak, A. & Schwinghamme, J. (2013). Step-Indexed Relational Reasoning for Countable Nondeterminism. Logical Methods in Computer Science, 9(4), Article 4. https://doi.org/10.2168/LMCS-9(4:4)2013

Schwinghammer, J. & Birkedal, L. (2011). Step-indexed relational reasoning for countable nondeterminism. In M. Bezem (Ed.), Computer Science Logic (CSL'11) : 25th International Workshop/20th Annual Conference of the EACSL (pp. 512-524). Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2011.512

Bizjak, A. & Birkedal, L. (2015). Step-indexed logical relations for probability. In A. Pitts (Ed.), Foundations of Software Science and Computation Structures: 18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings (pp. 279-294 ). Springer VS. https://doi.org/10.1007/978-3-662-46678-0_18

Aguirre, A. & Birkedal, L. (2023). Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice. Proceedings of the ACM on Programming Languages , 7, 33-60. Article 2. https://doi.org/10.1145/3571195

Birkedal, L., Reus, B., Schwinghammer, J., Støvring, K., Thamsborg, J. J. & Yang, H. (2011). Step-Indexed Kripke Models over Recursive Worlds. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, Texas, USA (pp. 119-132). Association for Computing Machinery.

Møller, A., Olesen, M. Ø. & Schwartzbach, M. I. (2007). Static Validation of XSL Transformations. A C M Transactions on Programming Languages and Systems, 29(4), Article 21. https://doi.org/10.1145/1255450.1255454

Brabrand, C., Møller, A. & Schwartzbach, M. I. (2001). Static Validation of Dynamically Generated HTML. In Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering (pp. 38-45). Association for Computing Machinery. https://doi.org/10.1145/379605.379657

Vorreiter Pedersen, M. & Askarov, A. (2019). Static Enforcement of Security in Runtime Systems. In Proceedings - 2019 IEEE 32nd Computer Security Foundations Symposium, CSF 2019 (pp. 335-350). Article 8823712 IEEE. https://doi.org/10.1109/CSF.2019.00030

Stein, B., Nielsen, B. B., Chang, B.-Y. E. & Møller, A. (2019). Static Analysis with Demand-driven Value Refinement. Proceedings of the ACM on Programming Languages , 3(OOPSLA), Article 140. https://doi.org/10.1145/3360566

Kirkegaard, C., Møller, A. & Schwartzbach, M. I. (2004). Static Analysis of XML Transformations in Java. I E E E Transactions on Software Engineering, 30(3), 181-192. https://doi.org/10.1109/TSE.2004.1271173

Madsen, M. (2015). Static Analysis of Dynamic Languages. Department of Computer Science, Aarhus University.

Displaying results 51 to 100 out of 533

Revised 05.12.2025

Marianne Dammand Iversen