Publications

Sort by: Date | Author | Title

Penninckx, W., Timany, A. & Jacobs, B. (2019). Abstract I/O Specification. ArXiv. http://arxiv.org/abs/1901.10541v1

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

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

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

Oortwijn, W., Huisman, M., Joosten, S. J. C. & van de Pol, J. (2020). Automated verification of parallel nested DFS. In A. Biere & D. Parker (Eds.), Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I (pp. 247-265). Springer. https://doi.org/10.1007/978-3-030-45190-5_14

Niss, H. & Birkedal, L. (Eds.) (2004). Context-aware computing: proceedings of conference on Context-aware Computing, Copenhagen, November 30, 2004. IT University of Copenhagen.

Nieto, A., Gondelman, L., Reynaud, A., Timany, A. & Birkedal, L. (2022). Modular verification of op-based CRDTs in separation logic. Proceedings of the ACM on Programming Languages , 6(OOPSLA2), 1788-1816. Article 188. https://doi.org/10.1145/3563351

Nieto, A., Daby-Seesaram, A., Gondelman, L., Timany, A. & Birkedal, L. (2023). Modular Verification of State-Based CRDTs in Separation Logic. In K. Ali & G. Salvaneschi (Eds.), 37th European Conference on Object-Oriented Programming, ECOOP 2023 Article 22 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ECOOP.2023.22

Nielsen, J. B. & Spitters, B. (2019). Smart Contract Interactions in Coq. (0 ed.) ArXiv.

Nielsen, J. B. & Spitters, B. (2020). Smart contract interactions in coq. In E. Sekerinski, N. Moreira, J. N. Oliveira, D. Ratiu, R. Guidotti, M. Farrell, M. Luckcuck, D. Marmsoler, J. Campos, T. Astarte, L. Gonnord, A. Cerone, L. Couto, B. Dongol, M. Kutrib, P. Monteiro & D. Delmas (Eds.), Formal Methods- FM 2019 International Workshops - Revised Selected Papers (pp. 380-391). Springer. https://doi.org/10.1007/978-3-030-54994-7_29

Nielsen, E. H., Annenkov, D. & Spitters, B. (2023). Formalising Decentralised Exchanges in Coq. In R. Krebbers, D. Traytel, B. Pientka & S. Zdancewic (Eds.), CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 290-302). Association for Computing Machinery. https://doi.org/10.1145/3573105.3575685

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

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

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

Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P. & Birkedal, L. (2008). Ynot: Depent Types for Imperative Programs. In International Conference on Functional Programming: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, (Vol. session 9, pp. 229-240). Association for Computing Machinery.

Nanevski, A., Ahmed, A., Morrisett, G. & Birkedal, L. (2007). Abstract predicates and mutable ADTs in hoare type theory. In R. D. Nicola (Ed.), Programming Languages and Systems: 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007. Proceedings (pp. 189-204). Springer VS. https://doi.org/10.1007/978-3-540-71316-6_14

Nanevski, A., Morrisett, G. & Birkedal, L. (2006). Polymorphism and separation in Hoare type theory. SIGPLAN Notices, 41(9), 62-73. https://doi.org/10.1145/1160074.1159812

Møgelberg, R. E., Birkedal, L. & Petersen, R. L. (2007). Domain theoretic models of parametric polymorphism. Theoretical Computer Science, 388(1-3), 152-172. https://doi.org/10.1016/j.tcs.2007.06.016

Møgelberg, R. E. & Birkedal, L. (2005). Categorical Models of Abadi-Plotkin's logic for parametricity. Mathematical Structures in Computer Science, 15(4), 709-772.

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. & 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

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

Milo, M., Nielsen, E. H., Annenkov, D. & Spitters, B. (2022). Finding smart contract vulnerabilities with ConCert's property-based testing framework. FMBC: Formal Methods for Blockchains https://doi.org/10.48550/arXiv.2208.00758

Milo, M., Nielsen, E. H., Annenkov, D. & Spitters, B. (2022). Finding Smart Contract Vulnerabilities with ConCert's Property-Based Testing Framework. In Z. Dargaye & C. Schneidewind (Eds.), 4th International Workshop on Formal Methods for Blockchains (FMBC 2022) Dagstuhl Publishing. https://doi.org/10.4230/OASIcs.FMBC.2022.2

Meijer, J. & van de Pol, J. (2019). Sound black-box checking in the LearnLib. Innovations in Systems and Software Engineering, 15(3-4), 267-287. https://doi.org/10.1007/s11334-019-00342-6

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

Mehnert, H., Sieczkowski, F., Birkedal, L. & Sestoft, P. (2012). Formalized verification of snapshotable trees: Separation and sharing. In R. Joshi, P. Müller & A. Podelski (Eds.), Verified Software: Theories, Tools, Experiments: 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings (pp. 179-195). Springer. https://doi.org/10.1007/978-3-642-27705-4_15

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

Makarov, E. & Spitters, B. (2013). The Picard algorithm for ordinary differential equations in Coq. In Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings (pp. 463-468) https://doi.org/10.1007/978-3-642-39634-2_34

Madsen, M. & Pol, J. V. D. (2020). Polymorphic types and effects with Boolean unification. In Proceedings of the ACM on Programming Languages (OOPSLA ed., Vol. 4). Association for Computing Machinery. https://doi.org/10.1145/3428222

Madsen, M. & Van De Pol, J. (2021). Relational nullable types with Boolean unification. Proceedings of the ACM on Programming Languages , 5(OOPSLA), 1-28. Article 110. https://doi.org/10.1145/3485487

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

Madsen, M. & Pol, J. V. D. (2023). Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism. In K. Ali & G. Salvaneschi (Eds.), 37th European Conference on Object-Oriented Programming (ECOOP 2023) Article 18 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ECOOP.2023.18

Liu, Z., Stepanenko, S., Pichon-Pharabod, J., Timany, A., Askarov, A. & Birkedal, L. (2023). VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A. Proceedings of the ACM on Programming Languages , 7, 1438-1462. https://doi.org/10.1145/3591279

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

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

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

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

Krogh-Jespersen, M., Timany, A., Ohlenbusch, M. E., Gregersen, S. O. & Birkedal, L. (2020). Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. In P. Müller (Ed.), Programming Languages and Systems- 29th European Symposium on Programming ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings (pp. 336-365). Springer. https://doi.org/10.1007/978-3-030-44914-8_13

Krishnaswami, N., Birkedal, L. & Aldrich, J. (2010). Verifying event-driven programs using ramified frame properties. In A. Kennedy & N. Benton (Eds.), {Proceedings of TLDI 2010: 2010 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Madrid, Spain, January 23, 2010 (pp. 63-76). Association for Computing Machinery. https://doi.org/10.1145/1708016.1708025

Krishnaswami, N. R., Aldrich, J., Birkedal, L., Svendsen, K. & Buisse, A. (2009). Design patterns in separation logic. In A. Kennedy & A. Ahmed (Eds.), Proceedings of the 2009 ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI'09 (pp. 105-115). Association for Computing Machinery. https://doi.org/10.1145/1481861.1481874

Krishnaswam, N. R. K., Aldrich, J. & Birkedal, L. (2007). Modular Verification of the Subject-Observer Pattern via Higher-order Separation Logic. In Proceedings of 9th Workshop on Formal Techniques for Java-like Programs, FTfJP Fakultät für Informatik, Universität Magdeburg. http://www.cs.cmu.edu/~neelk/observer.pdf

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

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

Krebbers, R. & Spitters, B. (2013). Type classes for efficient exact real arithmetic in CoQ. Logical Methods in Computer Science, 9(1). https://doi.org/10.2168/LMCS-9(1:01)2013

Krebbers, R. & Spitters, B. (2011). Computer certified efficient exact reals in Coq. In Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011 and 10th International Conference, MKM 2011, Proceedings (pp. 90-106) https://doi.org/10.1007/978-3-642-22673-1_7

Krebbers, R., Jourdan, J.-H., Jung, R., Tassarotti, J., Kaiser, J.-O., Timany, A., Charguéraud, A. & Dreyer, D. (2018). MoSeL: a general, extensible modal framework for interactive proofs in separation logic. PACMPL, 2(ICFP), 77:1-77:30. Article 3236772. https://doi.org/10.1145/3236772

Kordon, F., Leuschel, M., Pol, J. V. D. & Thierry-Mieg, Y. (2019). Software Architecture of Modern Model Checkers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): State of the Art and Perspectives (pp. 393-419). Springer. https://doi.org/10.1007/978-3-319-91908-9_20

Khurana, S., Schivo, S., Plass, J. R. M., Mersinis, N., Scholma, J., Kerkhofs, J., Zhong, L., van de Pol, J., Langerak, R., Geris, L., Karperien, M. & Post, J. N. (2021). An ECHO of Cartilage: In Silico Prediction of Combinatorial Treatments to Switch Between Transient and Permanent Cartilage Phenotypes With Ex Vivo Validation. Frontiers in Bioengineering and Biotechnology, 9, Article 732917. https://doi.org/10.3389/fbioe.2021.732917

Kavvos, G. A. & Gratzer, D. (2023). Under Lock and Key: A Proof System for a Multimodal Logic. Bulletin of Symbolic Logic, 29(2), 264-293. https://doi.org/10.1017/bsl.2023.14

Displaying results 101 to 150 out of 345

Revised 17.04.2023

Sofia Hedegaard Rasmussen