Publications

Sort by: Date | Author | Title

Thamsborg, J. J. & Birkedal, L. (2011). A Kripke Logical Relation for Effect-Based Program Transformations. In ICFP 11. Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (pp. 445-456). Association for Computing Machinery. https://doi.org/10.1145/2034574.2034831

Chatzigiannakis, I., Michail, O., Nikolaou, S., Pavlogiannis, A. & Spirakis, P. G. (2011). All Symmetric Predicates in NSPACE(n 2) Are Stably Computable by the Mediated Population Protocol Model. Lecture Notes in Computer Science, 6281, 270. https://doi.org/10.1007/978-3-642-15155-2_25

Schwinghammer, J., Birkedal, L. & Støvring, K. (2011). A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces. In M. Hofmann (Ed.), Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26–April 3, 2011. Proceedings (pp. 305-319). Springer. https://doi.org/10.1007/978-3-642-19805-2_21

Buisse, A., Birkedal, L. & Støvring, K. (2011). A Step-Indexed Kripke Model of Separation Logic for Storable Locks. Electronic Notes in Theoretical Computer Science, 276. https://doi.org/10.1016/j.entcs.2011.09.018

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

Birkedal, L., Møgelberg, R. E., Støvring, K. & schwinghammer, J. (2011). First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Annual Symposium on Logic in Computer Science, 55-64. https://doi.org/10.1109/LICS.2011.16

Møller, A. & Schwarz, M. R. (2011). HTML Validation of Context-Free Languages. Lecture Notes in Computer Science, 6604, 426-440. https://doi.org/10.1007/978-3-642-19805-2_29

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

Jensen, S. H., Madsen, M. & Møller, A. (2011). Modeling the HTML DOM and Browser API in Static Analysis of JavaScript Web Applications. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering. ESEC/FSE '11 (pp. 59-69). Association for Computing Machinery. https://doi.org/10.1145/2025113.2025125

Jensen, J. B., Birkedal, L. & Sestoft, P. (2011). Modular Verification of Linked Lists with Views via Separation Logic. Journal of Object Technology, 10(1), 21-40. https://doi.org/10.5381/jot.2011.10.1.a2

Schwinghammer, J., Birkedal, L., Reus, B. & Yang, H. (2011). Nested Hoare Triples and Frame Rules for Higher-Order Store. Logical Methods in Computer Science, 7(3:21), 440-454. https://doi.org/10.2168/LMCS-7(3:21)2011

Svendsen, K., Birkedal, L. & Nanevski, A. (2011). Partiality, State, and Dependent Types. In Proceedings of Typed LAmbda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011 (Vol. LNCS 6690, pp. 198-212). Springer.

Feldthaus, A., Millstein, T., Møller, A., Schäfer, M. & Tip, F. (2011). Refactoring towards the good parts of JavaScript. Poster session presented at SPLASH 2011, Portland, Oregon, United States. https://doi.org/10.1145/2048147.2048200

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.

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

Feldthaus, A., Millstein, T., Møller, A., Schäfer, M. & Tip, F. (2011). Tool-supported Refactoring for JavaScript. In Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications (pp. 119-138). Association for Computing Machinery. https://doi.org/10.1145/2048066.2048078

Bengtson, J., Jensen, J. B., Sieczkowski, F. & Birkedal, L. (2011). Verifying object-oriented programs with higher-order separation logic in Coq. In M. V. Eekelen , H. Geuvers, J. Schmaltz & F. Wiedijk (Eds.), Interactive Theorem Proving: Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings (pp. 22-38). Springer. https://doi.org/10.1007/978-3-642-22863-6_5

Møller, A. & Schwartzbach, M. I. (2011). XML Graphs in Program Analysis. Science of Computer Programming, 76(6), 492-515. https://doi.org/10.1016/j.scico.2009.11.007

Ahmed, A. (Ed.), Benton, N. (Ed.) & Birkedal, L. (2010). 10351 Abstracts Collection Modelling, Controlling and Reasoning About State: Dagstuhl Seminar . Dagstuhl Publishing. Dagstuhl Seminar Proceedings Vol. 10351 http://drops.dagstuhl.de/opus/volltexte/2010/2811/

Birkedal, L., Swinghammer, J. & Støvring, K. (2010). A Metric Model of Lambda Calculus with Guarded Recursion. In L. Santocanale (Ed.), Fixed Points in Computer Science 2010: Brno, August 21-22, 2010 http://www.diku.dk/~stovring/papers/metric-model-guarded-recursion.pdf

Brabrand, C., Giegerich, R. & Møller, A. (2010). Analyzing Ambiguity of Context-Free Grammars. Science of Computer Programming, 75(3), 176-191. https://doi.org/10.1016/j.scico.2009.11.002

Glenstrup, A. J., Damgaard, T. C., Birkedal, L. & Højsgaard, E. (2010). An Implementation of Bigraph Matching. (TR 2010-135 ed.) IT-Universitetet i København.

Dreyer, D., Neis, G., Rossberg, A. & Birkedal, L. (2010). A relational modal logic for higher-order stateful ADTs. In M. Hermenegildo & J. Palsberg (Eds.), Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010 (pp. 185-198). Association for Computing Machinery. https://doi.org/10.1145/1706299.1706323

Schwinghammer, J., Yang, H., Birkedal, L., Pottier, F. & Reus, B. (2010). A semantic foundation for hidden state. In L. Ong (Ed.), Foundations of Software Science and Computational Structures: 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings (pp. 2-17). Springer. https://doi.org/10.1007/978-3-642-12032-9_2

Jensen, S. H., Møller, A. & Thiemann, P. (2010). Interprocedural Analysis with Lazy Propagation. Lecture Notes in Computer Science, 6337, 320-339. https://doi.org/10.1007/978-3-642-15769-1_20

Jensen, J. B., Birkedal, L. & Sestoft, P. (2010). Modular verification of linked lists with views via separation logic. In Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs (pp. 4:1--4:7). Association for Computing Machinery. https://doi.org/10.1145/1924520.1924524

Jensen, J. B., Birkedal, L. & Sestoft, P. (2010). Modular verification of linked lists with views via separation logic. In FTFJP '10. Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs Article 4 Association for Computing Machinery. https://doi.org/10.1145/1924520.1924524

Birkedal, L., Støvring, K. & Thamsborg, J. J. (2010). Realisability semantics of parametric polymorphism, general references and recursive types. Mathematical Structures in Computer Science, 20(4), 655-703.

Birkedal, L., Støvring, K. & Thamsborg, J. (2010). Realisability semantics of parametric polymorphism, general references and recursive types. Mathematical Structures in Computer Science, 20(4), 655-703. https://doi.org/10.1017/S0960129510000162

Birkedal, L., Støvring, K. & Thamsborg, J. (2010). Realizability semantics of parametric polymorphism, general references, and recursive types. Mathematical Structures in Computer Science, 20(4), 655-703. https://doi.org/10.1017/S0960129510000162

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.

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

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

Svendsen, K., Birkedal, L. & Parkinson, M. (2010). Verifying generics and delegates. In ECOOP 2010 – Object-Oriented Programming: 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings (pp. 175-199). Springer. https://doi.org/10.1007/978-3-642-14107-2_9

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

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

Møller, A. & Schwarz, M. R. (2009). JWIG: Yet Another Framework for Maintainable and Secure Web Applications. In J. Filipe & J. Cordeiro (Eds.), WEBIST 2009 - Proceedings of the Fifth International Conference on Web Information Systems and Technologies (pp. 47-53). Institute for Systems and Technologies of Information, Control and Communication.

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.

Schwinghammer, J., Birkedal, L., Reus, B. & Yang, H. (2009). Nested hoare triples and frame rules for higher-order store. In E. Grädel & R. Kahle (Eds.), Computer Science Logic: 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings (pp. 440-454). Springer. https://doi.org/10.1007/978-3-642-04027-6_32

Birkedal, L., Støvring, K. & Thamsborg, J. (2009). Realizability semantics of parametric polymorphism, general references, and recursive types. In L. D. Alfaro (Ed.), Foundations of Software Science and Computational Structures: 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings (pp. 456-470). Springer. https://doi.org/10.1007/978-3-642-00596-1_32

Birkedal, L., Støvring, K. & Thamsborg, J. J. (2009). Relational Parametricity for References and Recursive Types. In A. Kennedy & A. Ahmed (Eds.), Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009. (pp. 91-104). Association for Computing Machinery.

Birkedal, L., Støvring, K. & Thamsborg, J. (2009). Solutions of generalized recursive metric-space equations. In R. Matthes & T. Uustalu (Eds.), 6th Workshop on Fixed Points in Computer Science, FICS 2009: Coimbr a, P ortugal, 12-13 September 2009, Proceedings (pp. 18-24). Institute of Cybernetics at Tallinn University of Technology.

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/

Jensen, S. H., Møller, A. & Thiemann, P. (2009). Type Analysis for JavaScript. Lecture Notes in Computer Science, 5673, 238–255. https://doi.org/10.1007/978-3-642-03237-0_17

Petersen, R. L., Birkedal, L., Nanevski, A. & Morrisett, G. (2008). A realizability model for impredicative Hoare Type Theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4960 LNCS, pp. 337-352) https://doi.org/10.1007/978-3-540-78739-6_26

Birkedal, L., Reus, B., Schwinghammer, J. & Yang, H. (2008). A Simple Model of Separation Logic for Higher-order Store. Lecture Notes in Computer Science, 348-360.

Birkedal, L., Møgelberg, R. E. & Lerchedahl Petersen, R. (2008). Category-theoretic models of linear Abadi & Plotkin Logic. Theory and Applications of Categories, 20(7), 116-151.

Brabrand, C., Møller, A. & Schwartzbach, M. I. (2008). Dual Syntax for XML Languages. Information Systems, 33(4), 385-406. https://doi.org/10.1016/j.is.2008.01.006

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

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

Displaying results 401 to 450 out of 544

Revised 05.12.2025

Marianne Dammand Iversen