L. Birkedal, J. Schwinghammer, and K. Støvring. A step-indexed kripke model of hidden state via recursive properties on recursively defined metric spaces. To Appear at FICS 2010. (PDF, 224826 bytes)

J.B. Jensen, L. Birkedal, and P. Sestoft. Modular verification of linked lists with views via separation logic. In Proc. of FTfJP'2010, 2010. (PDF, 321793 bytes)

L. Birkedal, B. Reus, J. Schwinghammer, K. Støvring, J. Thamsborg, and H. Yang. Step-indexed kripke models over recursive worlds. 2010. Submitted for publication. (PDF, 544494 bytes)

K. Svendsen, L. Birkedal, and M. Parkinson. Verifying generics and delegates. December 2009. Accepted for publication in ECOOP 2010. (PDF, 266784 bytes)

J. Schwinghammer, H. Yang, L. Birkedal, F. Pottier, and B. Reus. A semantic foundation for hidden state. In Proceedings of FOSSACS 2010, October 2009. To Appear (accepted for publication). (PDF, 425026 bytes)

N. Krishnaswami, L. Birkedal, and J. Aldrich. Verifying event-driven programs using ramified frame properties. In Proceedings of TLDI'2010, 2010. To Appear. (PDF, 287590 bytes)

J. Schwinghammer, H. Yang, L. Birkedal, F. Pottier, and B. Reus. A semantic foundation for hidden state. October 2009. Submitted for publication. (PDF, 425026 bytes)

J. Schwinghammer, L. Birkedal, B. Reus, and H. Yang. Nested Hoare triples and frame rules for higher-order store. In Proceedings of CSL 2009, April 2009. (PDF, 332572 bytes)

N. Krishnaswami, J. Aldrich, L. Birkedal, K. Svendsen, and A. Buisse. Design patterns in separation logic. In Proc. of TLDI 2009, January 2009. (PDF, 236270 bytes)

K. Svendsen, A. Buisse, and L. Birkedal]. Verifying design patterns in Hoare type theory. Technical Report ITU-TR-2008-112, IT University of Copenhagen, September 2008. (PDF, 153241 bytes)

A. Nanevski, G. Morrisett, A. Shinnar, P. Goverau, and L. Birkedal. Ynot: Dependent types for imperative programs. In Proc. of ICFP 2008, Sep 2008. (PDF, 281368 bytes)

L. Birkedal, B. Reus, J. Schwinghammer, and H. Yang. A Simple Model of Separation Logic for Higher-order Store. In Proceedings of ICALP 2008, 2008. (PDF, 230384 bytes)

C. Varming and L. Birkedal. Higher-order separation logic in Isabelle/HOLCF. In Proceedings of MFPS 2008, 2008. (PDF, 305074 bytes)

R.L. Petersen, L. Birkedal, A. Nanevski, and G. Morrisett. A Realizability Model of Impredicative Hoare Type Theory. In Proceedings of ESOP 2008, 2008. (PDF, 285783 bytes)

A. Nanevski, G. Morrisett, and L. Birkedal. Hoare type theory, polymorphism and separation. Journal of Functional Programming, 2007. To Appear (accepted for publication). (PDF, 427897 bytes)

R.L. Petersen, L. Birkedal, A. Nanevski, and G. Morrisett. A Realizability Model of Impredicative Hoare Type Theory. Technical report, IT University of Copenhagen, 2007. (PDF, 231108 bytes)

N. Krishnaswami, J. Aldrich, and L. Birkedal. Modular verification of the subject-observer pattern via higher-order separation logic. In 9th Workshop on Formal Techniques for Java-like Programs (FTfJP 2007), 2007. (PDF, 196800 bytes)

B. Biering, L. Birkedal, and N. Torp-Smith. BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM Transactions on Programming Languages and Systems, 2007. (PDF, 368220 bytes)

L. Birkedal and H. Yang. Relational parametricity and separation logic. In Proceedings of FOSSACS 2007, 2007. (PDF, 249910 bytes)

A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal. Abstract predicates and mutable ADTs in Hoare type theory. In Proceedings of ESOP 2007, 2007. (PDF, 184378 bytes)

A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal. Abstract predicates and mutable ADTs in Hoare type theory. Technical Report TR-14-06, Harvard University, September 2006. (PDF, 371477 bytes)

L. Birkedal, N. Torp-Smith, and H. Yang. Semantics of separation-logic typing and higher-order frame rules for algol-like languages. Logical Methods in Computer Science, 2(5:1), August 2006. lmcs online version.

N. Torp-Smith, L. Birkedal, and J.C. Reynolds. Local reasoning about a copying garbage collector. ACM Transactions on Programming Languages and Systems, 2006. To Appear. (PDF, 430789 bytes)

A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and separation in hoare type theory. In Julia Lawall, editor, Proceedings of ICFP 2006, September 2006. To appear. (PDF, 324596 bytes)

A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and separation in hoare type theory. Technical Report TT-10-06, Harvard University, April 2006. (PDF, 416968 bytes)

B. Biering, L. Birkedal, and N. Torp-Smith. BI-hyperdoctrines, higher-order separation logic, and abstra ction. Technical Report ITU-TR-2005-69, IT University of Copenhagen, July 2005. (PDF, 405778 bytes)

L. Birkedal and N. Torp-Smith. Higher-order separation logic and abstraction. February 2005. Manuscript. (Gzipped PostScript, 13 pages, 163758 bytes)

L. Birkedal, N. Torp-Smith, and H. Yang. Semantics of separation-logic typing and higher-order frame rules. In Proceedings of the 20th IEEE Symposium of Logic in Computer Science (LICS'05), pages 260-269, Chicago, IL, USA, June 2005. (PDF, 195392 bytes)

B. Biering, L. Birkedal, and N. Torp-Smith. Bi hyperdoctrines and higher-order separation logic. In In Proceedings of European Symposium on Programming, volume 3444 of LNCS, pages 233-247, 2005. (PDF, 161526 bytes)

L. Birkedal, N. Torp-Smith, and J.C. Reynolds. Local reasoning about a copying garbage collector. In Proceedings of the 31-st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 220-231. ACM Press, January 2004. (Gzipped PostScript, 12 pages, 109058 bytes)

L. Birkedal, N. Torp-Smith, and J.C. Reynolds. Correctness of a garbage collector via local reasoning. Technical Report 30, The IT University of Copenhagen, Copenhagen, Denmark, July 2003. (Gzipped PostScript, 62 pages, 199335 bytes)