Publications

Sort by: Date | Author | Title

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

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

Mezzetti, G., Møller, A. & Torp, M. T. (2018). Type Regression Testing to Detect Breaking Changes in Node.js Libraries. In T. D. Millstein (Ed.), 32nd European Conference on Object-Oriented Programming, ECOOP 2018 (Vol. 109, pp. 7:1-7:24). Article 7 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ECOOP.2018.7

Pavlogiannis, A., Tkadlec, J., Chatterjee, K. & Nowak, M. A. (2017). Amplification on Undirected Population Structures: Comets Beat Stars. Scientific Reports, 7(1), 82. Article 82. https://doi.org/10.1038/s41598-017-00107-w

Krogh-Jespersen, M., Svendsen, K. & Birkedal, L. (2017). A relational model of types-and-effects in higher-order concurrent separation logic. In POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages: POPL 2017 (pp. 218-231). Association for Computing Machinery. https://doi.org/10.1145/3009837.3009877

Spencer, B., Benedikt, M., Møller, A. & Breugel, F. V. (2017). ArtForm: A Tool for Exploring the Codebase of Form-based Websites. In K. Sen & T. Bultan (Eds.), ISSTA 2017 - Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (pp. 380-383). Association for Computing Machinery. https://doi.org/10.1145/3092703.3098226

Andreasen, E., Gong, L., Møller, A., Pradel, M., Selakovic, M., Sen, K. & Staicu, C.-A. (2017). A Survey of Dynamic Analysis and Test Generation for JavaScript. A C M Computing Surveys, 50(5), 66:1-66:36. Article 66. https://doi.org/10.1145/3106739

Dinsdale-Young, T., da Rocha Pinto, P., Andersen, K. J. A. & Birkedal, L. (2017). Caper: Automatic Verification for Fine-Grained Concurrency. 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: 26th European Symposium on Programming, ESOP 2017 (Vol. 10201, pp. 420-447). Springer VS. https://doi.org/10.1007/978-3-662-54434-1_16

Pedersen, M. V. & Askarov, A. (2017). From Trash to Treasure: Timing-Sensitive Garbage Collection. In 2017 IEEE Symposium on Security and Privacy, SP 2017 - Proceedings (pp. 693-709). Article 7958605 IEEE Computer Society Press. https://doi.org/10.1109/SP.2017.64

Kristensen, E. K. & Møller, A. (2017). Inference and Evolution of TypeScript Declaration Files. In M. Huisman & J. Rubin (Eds.), Fundamental Approaches to Software Engineering - 20th International Conference, FASE 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings: 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings (Vol. 10202, pp. 99-115). Springer VS. https://doi.org/10.1007/978-3-662-54494-5_6

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

Ernst, E., Møller, A., Schwarz, M. & Strocco, F. (2017). Message safety in Dart. Science of Computer Programming, 133/1(1), 51-73. https://doi.org/10.1016/j.scico.2016.06.006

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

Adamsen, C. Q., Møller, A. & Tip, F. (2017). Practical Initialization Race Detection for JavaScript Web Applications. Proceedings of the ACM on Programming Languages , 1(OOPSLA), 66:1-66:22. Article 66. https://doi.org/10.1145/3133890

Midtgaard, J. & Møller, A. (2017). QuickChecking static analysis properties. Software Testing, Verification and Reliability, 27(6), Article e1640. https://doi.org/10.1002/stvr.1640

Adamsen, C. Q., Møller, A., Karim, R., Sridharan, M., Tip, F. & Sen, K. (2017). Repairing Event Race Errors by Controlling Nondeterminism. In Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering, ICSE 2017 (pp. 289-299). Article 7985670 IEEE Press. https://doi.org/10.1109/ICSE.2017.34

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

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

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

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

Kristensen, E. K. & Møller, A. (2017). Type Test Scripts for TypeScript Testing. Proceedings of the ACM on Programming Languages , 1(OOPSLA), 90:1-90:25. Article 90. https://doi.org/10.1145/3133914

Birkedal, L., Jaber, G., Sieczkowski, F. & Thamsborg, J. (2016). A Kripke logical relation for effect-based program transformations. Information and Computation, 249, 160-189. https://doi.org/10.1016/j.ic.2016.04.003

Adamsen, C. Q., Mezzetti, G. & Møller, A. (2016). Analyzing Test Completeness for Dynamic Languages. In ISSTA 2016 - Proceedings of the 25th International Symposium on Software Testing and Analysis: ISSTA 2016 (pp. 142-153). Association for Computing Machinery. https://doi.org/10.1145/2931037.2931059

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

Madsen, M., Tip, F., Andreasen, E. S., Sen, K. & Møller, A. (2016). Feedback-directed instrumentation for deployed JavaScript applications. In Proceedings - 2016 IEEE/ACM 38th IEEE International Conference on Software Engineering Companion, ICSE 2016: ICSE 2016 (pp. 899-910). Association for Computing Machinery. https://doi.org/10.1145/2884781.2884846

Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H. B., Spitters, B. & Vezzosi, A. (2016). Guarded cubical type theory. Abstract from 22nd International Conference on Types for Proofs and Programs, Novi Sad, Serbia. http://www.cs.au.dk/~spitters/TYPES16.pdf

Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H. B., Spitters, B. & Vezzosi, A. (2016). Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In J.-M. Talbot & L. Regnier (Eds.), CSL 2016: 25th EACSL Annual Conference on Computer Science Logic (pp. 1 - 17)

Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H. B., Spitters, B. & Vezzosi, A. (2016, Aug 1). Guarded Cubical Type Theory. https://doi.org/10.4230/LIPIcs.CSL.2016.23

Bizjak, A., Grathwohl, H. B., Clouston, R., Møgelberg, R. E. & Birkedal, L. (2016). Guarded dependent type theory with coinductive types. In B. Jacobs & C. Löding (Eds.), Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016 (Vol. 9634, pp. 20-35). Springer VS. https://doi.org/10.1007/978-3-662-49630-5_2

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

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

Chatterjee, K., Ibsen-Jensen, R. R. & Pavlogiannis, A. (2016). Optimal Reachability and a Space-Time Tradeoff for Distance Queries in Constant-Treewidth Graphs. In 24th Annual European Symposium on Algorithms (ESA 2016) (pp. 28:1-28:17). Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ESA.2016.28

Birkedal, L. (2016). Preface. Electronic Notes in Theoretical Computer Science, 325, 1-2. https://doi.org/10.1016/j.entcs.2016.09.028

Devriese, D., Birkedal, L. & Piessens, F. (2016). Reasoning about object capabilities with logical relations and effect parametricity. In 2016 IEEE European Symposium on Security and Privacy, EURO S and P 2016 (pp. 147-162). Article 7467352 IEEE Press. https://doi.org/10.1109/EuroSP.2016.22

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

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

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

Heinze, T. S., Møller, A. & Strocco, F. (2016). Type safety analysis for dart. In R. Ierusalimschy (Ed.), DLS 2016 - Proceedings of the 12th Symposium on Dynamic Languages (pp. 1-12). Association for Computing Machinery. https://doi.org/10.1145/2989225.2989226

Mezzetti, G., Møller, A. & Strocco, F. (2016). Type unsoundness in practice: An empirical study of dart. In R. Ierusalimschy (Ed.), DLS 2016 - Proceedings of the 12th Symposium on Dynamic Languages (pp. 13-24). Association for Computing Machinery. https://doi.org/10.1145/2989225.2989227

Dodds, M., Jagannathan, S., Parkinson, M. J., Svendsen, K. & Birkedal, L. (2016). Verifying custom synchronisation constructs using higher-order separation logic. ACM Transactions on Programming Languages and Systems, 38/2(2), 4:1 - 4:72. Article 4. https://doi.org/10.1145/2818638

Paviotti, M., Møgelberg, R. E. & Birkedal, L. (2015). A model of PCF in guarded type theory. Electronic Notes in Theoretical Computer Science, 319, 333–349. https://doi.org/10.1016/j.entcs.2015.12.020

Sieczkowski, F., Svendsen, K., Birkedal, L. & Pichon-Pharabod, J. (2015). A separation logic for fictional sequential consistency. In J. Vitek (Ed.), Programming Languages and Systems : 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 (pp. 736-761). Springer. https://doi.org/10.1007/978-3-662-46669-8_30

Pavlogiannis, A., Chatterjee, K., Adlam, B. & Nowak, M. A. (2015). Cellular cooperation with shift updating and repulsion. Scientific Reports, 5, 17147. https://doi.org/10.1038/srep17147

Askarov, A., Moore, S., Dimoulas, C. & Chong, S. (2015). Cryptographic Enforcement of Language-Based Information Erasure. In L. Viganò (Ed.), 28th IEEE Computer Security Foundations Symposium CSF 2015 : Proceedings (pp. 334-348). IEEE Computer Society Press. https://doi.org/10.1109/CSF.2015.30

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

Bizjak, A., Grathwohl, H. B., Clouston, R., Birkedal, L. & Møgelberg, R. E. (2015). Guarded dependent type theory with coinductive types. In Foundations of Software Science and Computation Structures Springer. https://doi.org/10.1007/978-3-662-49630-5_2

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

Livshits, B., Sridharan, M., Smaragdakis, Y., Lhoták, O., Amaral, J. N., Chang, B.-Y. E., Guyer, S. Z., Khedker, U. P., Møller, A. & Vardoulakis, D. (2015). In Defense of Soundiness: A Manifesto. Communications of the A C M, 58(2). https://doi.org/10.1145/2644805

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

Ernst, E., Schwarz, M. R., Strocco, F. & Møller, A. (2015). Message Safety in Dart. In Dynamic Languages Symposium 2015, DLS http://cs.au.dk/~amoeller/papers/fletch/paper.pdf

Displaying results 301 to 350 out of 545

Revised 05.12.2025

Marianne Dammand Iversen