N. Benton, L. Birkedal, A. Kennedy, and C. Varming. Formalizing domains, ultrametric spaces and semantics of programming languages. 2010. Submitted for publication. Coq Script: domultracoq.zip . (PDF, 874071 bytes)

L. Birkedal, J. Schwinghammer, and K. Støvring. A metric model of guarded recursion. 2010. To Appear at FICS 2010. (PDF, 159942 bytes)

L. Birkedal, K. Støvring, and J. Thamsborg. Realizability semantics of parametric polymorphism, general references, and recursive types. Mathematical Structures in Computer Science, May 2010. To Appear (accepted for publication). (PDF, 594721 bytes)

D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. In Proc. of ICFP 2010, 2010. To Appear (Accepted for publication). (PDF, 227422 bytes)

L. Birkedal, K. Støvring, and J. Thamsborg. A relational realizability model for higher-order stateful ADTs. March 2010. Submitted for publication. (PDF, 378294 bytes)

D. Dreyer, A. Ahmed, and L. Birkedal. Logical step-indexed logical relations. January 2010. Submitted for publication. (PDF, 304902 bytes)

L. Birkedal, K. Støvring, and J. Thamsborg. The category-theoretic solution of recursive metric-space quations. Technical Report ITU-2009-119, IT University of Copenhagen, 2009. (PDF, 369438 bytes)

D. Dreyer, G. Neis, A. Rossberg, and L. Birkedal. A relational modal logic for higher-order stateful ADTs. July 2009. To Appear in POPL'2010 (accepted for publication). (PDF, 339559 bytes)

L. Birkedal, K. Støvring, and J. Thamsborg. Solutions of generalized recursive metric-space equations. In Proceedings of FICS 2009, September 2009. (PDF, 76433 bytes)

D. Dreyer, A. Ahmed, and L. Birkedal. Logical step-indexed logical relations. In Proceedings of LICS 2009, August 2009. (PDF, 238714 bytes)

L. Birkedal, K. Støvring, and J. Thamsborg. Realizability semantics of parametric polymorphism, references, and recursive types. In Proceedings of FOSSACS'09, April 2009. (PDF, 258769 bytes)

L. Birkedal, K. Støvring, and J. Thamsborg. Relational parametricity for references and recursive types. In Proceedings of TLDI, January 2009. (PDF, 275897 bytes)

L. Birkedal, R.L. Petersen, R. Møgelberg, and C. Varming. Operational semantics and models of Linear Abadi-Plotkin Logic. 2008. Submitted for publication.

N. Bohr and L. Birkedal. Relational reasoning for recursive types and references. In Proceedings of APLAS 2006, June 2006. (PDF, 255966 bytes)

L. Birkedal, R.L. Petersen, R. Møgelberg, and C. Varming. Operational semantics and models of Linear Abadi & Plotkin Logic. June 2006. Submitted for publication. (PDF, 302365 bytes)

L. Birkedal and R.W. Harper. Constructing interpretations of recursives types in an operational setting. Information and Computation, 155:3-63, 1999. (Gzipped PostScript, 75 pages, 215811 bytes)

L. Birkedal and R.W. Harper. Constructing interpretations of recursive types in an operational setting (summary). In M. Abadi and I. Takayasu, editors, Theoretical Aspects of Computer Software: International Symposium, volume 1281 of Lecture Notes in Computer Science, pages 458-490, Sendai, Japan, September 1997. Springer. (Gzipped PostScript, 33 pages, 133503 bytes)