Publications

Chronological Listing (BibTeX database: BirkedalL.bib):
107 references, last updated Tue Jul 13 9:46:12 2010

[1]
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)

[2]
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)

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

[4]
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)

[5]
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)

[6]
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)

[7]
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)

[8]
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)

[9]
J. Thamsborg, L. Birkedal, and H. Yang. Two for the price of one: Lifting separation logic assertions. January 2010. Manuscript. (PDF, 284124 bytes)

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

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

[12]
L. Birkedal, K. Støvring, and J. Thamsborg. Realizability semantics of parametric polymorphism, general references, and recursive types. Technical Report TR-2010-124, IT University of Copenhagen, jan 2010. (PDF, 454483 bytes)

[13]
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)

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

[15]
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)

[16]
D. Dreyer, G. Neis, A. Rossberg, and L. Birkedal. A relational modal logic for higher-order stateful ADTs. In Proceedings of POPL'2010, January 2010. (PDF, 339667 bytes)

[17]
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)

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

[19]
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)

[20]
L. Birkedal, M. Bundgaard, S. Debois, T. Hildebrandt, and D. Grohmann. Higher-order contexts via games and the Int-construction. Technical Report ITU-TR-2009-117, IT University of Copenhagen, 2009. (PDF, 325715 bytes)

[21]
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)

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

[23]
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)

[24]
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)

[25]
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)

[26]
L. Birkedal, S. Debois, and T. Hildebrandt. On the construction of sorted bigraphical reactive systems. In Proc. of CONCUR 2008, Sep 2008. (PDF, 191985 bytes)

[27]
L. Birkedal, R.E. Møgelberg, and R.L. Petersen. Category-theoretic models of Linear Abadi & Plotkin Logic. Theory and Applications in Categories, 20(7):116-151, 2008. (PDF)

[28]
R.E. Møgelberg, L. Birkedal, and G. Rosolini. Synthetic domain theory and models of Linear Abadi & Plotkin Logic. Annals of Pure and Applied Logic, 2008. (PDF, 352147 bytes)

[29]
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)

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

[31]
L. Birkedal and H. Yang. Relational parametricity and separation logic. Logical Methods in Computer Science, 4(2:6):1-27, 2008. lmcs online version. (PDF, 285568 bytes)

[32]
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)

[33]
L. Birkedal, R.E. Møgelberg, and R.L. Petersen. Domain-theoretic models of parametric polymorphism. Theoretical Computer Science, 388(1-3):152-172, 2007. (PDF, 265619 bytes)

[34]
A.J. Glenstrup, T.C. Damgaard, L. Birkedal, and E. Højsgaard. An implementation of bigraph matching. 2007. Submitted for publication. (PDF, 326573 bytes)

[35]
T.C. Damgaard, A.J. Glenstrup, L. Birkedal, and R. Milner. An inductive characterization of matching in binding bigraphs. 2007. Submitted for publication. (PDF, 445771 bytes)

[36]
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)

[37]
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)

[38]
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)

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

[40]
L. Birkedal, T.C. Damgaard, A. Glenstrup, and R. Milner. Matching of bigraphs. In Proceedings of Graph Transformation for Verification and Concurrency 2006, Jan 2007. (PDF, 255029 bytes)

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

[42]
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)

[43]
L. Birkedal, R.E. Møgelberg, and R.L. Petersen. Linear Abadi and Plotkin logic. Logical Methods in Computer Science, 2(5:2), August 2006. lmcs online version.

[44]
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)

[45]
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.

[46]
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)

[47]
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)

[48]
L. Birkedal, S. Debois, and T. Hildebrandt. Sortings for reactive systems. In Christel Baier and Holger Hermanns, editors, Proceedings of CONCUR 2006, August 2006. (PDF, 168564 bytes)

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

[50]
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)

[51]
L. Birkedal, T.C. Damgaard, A. Glenstrup, and R. Milner. Matching of bigraphs. Technical Report ITU-TR-2006-88, IT University of Copenhagen, June 2006. (PDF, 219945 bytes)

[52]
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)

[53]
T.C. Damgaard and L. Birkedal. Axiomatizing binding bigraphs. Nordic Journal of Computing, 13(1-2):58-77, 2006. (PDF, 246862 bytes)

[54]
L. Birkedal, S. Debois, and T. Hildebrandt. Sortings for reactive systems. Technical Report 84, IT University of Copenhagen, Rued Langgards Vej 7, DK-2300 Copenhagen V, March 2006. (PDF, 261783 bytes)

[55]
L. Birkedal, M. Bundgaard, T.C. Damgaard, S. Debois, E. Elsborg, A.J. Glenstrup, T. Hildebrandt, R. Milner, and H. Niss. Bigraphical programming langauges for pervasive computing. In International Workshop on Combining Theory and Systems Building in Pervasive Computing. Position Paper., May 2006. (PDF, 109457 bytes)

[56]
L. Birkedal, S. Debois, E. Elsborg, T. Hildebrandt, and H. Niss. Bigraphical Models of Context-aware Systems. In Foundations of Software Science and Computation Structures (FOSSACS) 2006, number 3921 in Lecture Notes in Computer Science, March 2006. (PDF, 184412 bytes)

[57]
L. Birkedal, S. Debois, E. Elsborg, T. Hildebrandt, and H. Niss. Bigraphical Models of Context-aware Systems. Technical Report 74, IT University of Copenhagen, Rued Langgards Vej 7, DK-2300 Copenhagen V, November 2005. ISBN: 87-7949-110-3. (PDF, 179029 bytes)

[58]
T.C. Damgaard and L. Birkedal. Axiomatizing binding bigraphs (revised). Technical Report TR-2005-71, IT University of Copenhagen, March 2005. 36 pages. (PDF, 229885 bytes)

[59]
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)

[60]
T.C. Damgaard and L. Birkedal. Axiomatizing binding bigraphs. Technical Report TR-2005-65, IT University of Copenhagen, March 2005. 37 pages. (Gzipped PostScript, 37 pages, 186360 bytes) (PDF, 230806 bytes)

[61]
L. Birkedal and R.E. Møgelberg. Categorical models of Abadi-Plotkin's logic for parametricity. Mathematical Structures in Computer Science, 15:709-772, 2005. (Gzipped PostScript, 65 pages, 223379 bytes) (PDF, 605322 bytes)

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

[63]
L. Birkedal, R.E. Møgelberg, and R.L. Petersen. Parametric domain-theoretic models of polymorphic intuitionistic / linear lambda calculus. February 2005. Mathematical Foundations of Programming Semantics 2005. (PDF, 346581 bytes)

[64]
R.E. Møgelberg, L. Birkedal, and G. Rosolini. Synthetic domain theory and models of linear Abadi and Plotkin logic. February 2005. Mathematical Foundations of Programming Semantics 2005. (PDF, 362775 bytes)

[65]
L. Birkedal, R.E. Møgelberg, and R.L. Petersen. Parametric domain-theoretic models of linear Abadi-Plotkin logic. Technical Report TR-2005-57, IT University of Copenhagen, 2005. (Gzipped PostScript, 76 pages, 264426 bytes) (PDF, 539080 bytes)

[66]
R.E. Møgelberg, L. Birkedal, and G. Rosolini. Synthetic domain theory and models of linear Abadi and Plotkin logic. Technical Report TR-2005-59, IT University of Copenhagen, February 2005. (Gzipped PostScript, 52 pages, 224993 bytes) (PDF, 423219 bytes)

[67]
R.E. Møgelberg, L. Birkedal, and R.L. Petersen. Categorical models of PILL. Technical Report TR-2005-58, IT University of Copenhagen, February 2005. (Gzipped PostScript, 17 pages, 132842 bytes) (PDF, 205186 bytes)

[68]
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)

[69]
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)

[70]
J.Aa. Sørensen, K.J. Kristoffersen, A. Cervera, M. Schiøtz, T. Lynge, Z. Safar, and L. Birkedal. An infrastructure for context-dependent mobile multimedia communication. In Proceedings of 2004 IEEE International Workshop on Multimedia Signal Processing, September 2004. (PDF, 785298 bytes)

[71]
L. Birkedal. Bigraphical Programming Languages - a LaCoMoCo research project. In 2nd UK-Ubinet Workshop, Cambridge, UK, May 2004. Position Paper. (PDF, 48513 bytes)

[72]
L. Birkedal and R.E. Møgelberg. On the definition of parametricity. Technical Report 44, The IT University of Copenhagen, 2004. (Gzipped PostScript, 77 pages, 347573 bytes)

[73]
M. Tofte, L. Birkedal, M. Elsman, and N. Hallenberg. A retrospective on region-based memory management. Higher Order Symbolic Computation, 17(2), 2004. (Gzipped PostScript, 26 pages, 339574 bytes)

[74]
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)

[75]
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)

[76]
L. Birkedal. A general notion of realizability. Bulletin of Symbolic Logic, 8(2):266-282, 2002. (Gzipped PostScript, 17 pages, 141302 bytes)

[77]
M. Tofte, L. Birkedal, M. Elsman, N. Hallenberg, T.H. Olesen, and P. Sestoft. Programming with Regions in the ML Kit (for Version 4). The IT University of Copenhagen, September 2001. (234 pages). Available via http://www.it-c.dk/research/mlkit. (Gzipped PostScript, 234 pages, 611570 bytes)

[78]
L. Birkedal and J. van Oosten. Relative and modified relative realizability. Annals of Pure and Applied Logic, 118(1-2):115-132, 2002. (Gzipped PostScript, 18 pages, 102315 bytes)

[79]
S. Awodey and L. Birkedal. Elementary axioms for local maps of toposes. Journal of Pure and Applied Algebra, 177(3):215-230, February 2003. (Gzipped PostScript, 15 pages, 105682 bytes)

[80]
L. Birkedal. Developing theories of types and computability via realizability. Electronic Notes in Theoretical Computer Science, 34, 2000. Available at http://www.elsevier.nl/locate/entcs/volume34.html. The pdf version has active hyperreferences and is therefore the preferred version for reading online. (Gzipped PostScript, 290 pages, 624492 bytes) (PDF, 2023216 bytes)

[81]
L. Birkedal and J. van Oosten. Relative and modified relative realizability. Preprint 1146, Department of Mathematics, Universiteit Utrecht, March 2000. Superseded by  [78].

[82]
A. Bauer and L. Birkedal. Continuous functionals of dependent types and equilogical spaces. In P. Clote and H. Schwichtenberg, editors, Computer Science Logic, 14th Annual Conference of the EACSL, Fischbachau, Germany, August 21-26, 2000, volume 1862 of Lecture Notes in Computer Science. Springer, August 2000. (Gzipped PostScript, 15 pages, 89805 bytes)

[83]
L. Birkedal, J. van Oosten, G. Rosolini, and D.S. Scott, editors. Tutorial Workshop on Realizability Semantics, FLoC'99, Trento, Italy, 1999. Mathematical Structures in Computer Science, volume 12. Cambridge University Press, 2002.

[84]
S. Awodey, L. Birkedal, and D.S. Scott. Local realizability toposes and a modal logic for computability. Mathematical Structures in Computer Science, 12(3):319-334, 2002. (Gzipped PostScript, 16 pages, 106898 bytes)

[85]
L. Birkedal. Developing Theories of Types and Computability via Realizability. PhD thesis, School of Computer Science, Carnegie Mellon University, December 1999. Available as CMU Technical Report: CMU-CS-99-173. Superseded by  [80].

[86]
L. Birkedal. A general notion of realizability. In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, June 2000. IEEE Computer Society. To Appear. (Gzipped PostScript, 11 pages, 79119 bytes)

[87]
S. Awodey and L. Birkedal. Elementary axioms for local maps of toposes. Technical Report CMU-PHIL-103, Department of Philosophy, Carnegie Mellon University, November 1999. Submitted for Publication. (Gzipped PostScript, 18 pages, 68921 bytes)

[88]
S. Awodey, L. Birkedal, and D.S. Scott. Local realizability toposes and a modal logic for computability. In L. Birkedal, J. van Oosten, G. Rosolini, and D.S. Scott, editors, Tutorial Workshop on Realizability Semantics, FLoC'99, Trento, Italy, 1999, volume 23 of Electronic Notes in Theoretical Computer Science. Elsevier, 1999. Superseded by  [84]. (Gzipped PostScript, 14 pages, 67529 bytes)

[89]
S. Awodey, L. Birkedal, and D.S. Scott. Local realizability toposes and a modal logic for computability. Technical Report CMU-PHIL-99, Department of Philosophy, Carnegie Mellon University, April 1999. Superseded by  [84]. (Gzipped PostScript, 14 pages, 67529 bytes)

[90]
A. Bauer, L. Birkedal, and D.S. Scott. Equilogical spaces. Theoretical Computer Science, 315(1):35-59, 2004. (Gzipped PostScript, 28 pages, 134002 bytes)

[91]
L. Birkedal, A. Carboni, G. Rosolini, and D.S. Scott. Type theory via exact categories. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, pages 188-198, Indianapolis, Indiana, June 1998. IEEE Computer Society. (Gzipped PostScript, 11 pages, 50454 bytes)

[92]
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)

[93]
L. Birkedal and R.W. Harper. Constructing interpretations of recursives types in an operational setting. Technical Report CMU-CS-98-125, School of Computer Science, Carnegie Mellon University, April 1998. Superseded by  [92]. (Gzipped PostScript, 76 pages, 214371 bytes)

[94]
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. Superseded by  [92]. (Gzipped PostScript, 33 pages, 133503 bytes)

[95]
L. Birkedal and M. Tofte. A constraint-based region inference algorithm. Theoretical Computer Science, 258:299-392, 2001. (Gzipped PostScript, 106 pages, 229307 bytes)

[96]
M. Tofte and L. Birkedal. A region inference algorithm. ACM Transactions on Programming Languages and Systems, 20(4):734-767, July 1998. (plus 24 pages of electronic appendix). (Gzipped PostScript, 70 pages, 457058 bytes)

[97]
M. Tofte and L. Birkedal. Unification and polymorphism in region inference. To Appear in Milner Festschrift (Accepted), 1998. (25 pages). (Gzipped PostScript, 26 pages, 157287 bytes)

[98]
L. Birkedal, M. Tofte, and M. Vejlstrup. From region inference to von Neumann machines via region representation inference. In Proceedings of the 23-rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 171-183. ACM Press, January 1996. (Gzipped PostScript, 13 pages, 76740 bytes)

[99]
M. Tofte, L. Birkedal, M. Elsman, N. Hallenberg, T.H. Olesen, P. Sestoft, and P. Bertelsen. Programming with regions in the ML Kit (for version 3). Technical Report 98/25, Department of Computer Science, University of Copenhagen, November 1998. (214 pages). (Gzipped PostScript, 215 pages, 618135 bytes)

[100]
M. Tofte, L. Birkedal, M. Elsman, N. Hallenberg, T.H. Olesen, P. Sestoft, and P. Bertelsen. Programming with regions in the ML Kit. Technical Report 97/12, Department of Computer Science, University of Copenhagen, 1997. (194 pages). (Gzipped PostScript, 195 pages, 1996189 bytes)

[101]
L. Birkedal, N. Rothwell, M. Tofte, and D.N. Turner. The ML Kit, Version 1. Technical Report 93/14, Department of Computer Science, University of Copenhagen, 1993. (112 pages). (Gzipped PostScript, 119 pages, 213540 bytes)

[102]
L. Birkedal and M. Welinder. Binding-time analysis for Standard ML. Lisp and Symbolic Computation, 8(3):191-208, September 1995. (Gzipped PostScript, 18 pages, 68749 bytes)

[103]
L. Birkedal and M. Welinder. Binding-time analysis for Standard ML. In PEPM '94. ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation. Technical Report 94/9, Department of Computer Science, The University of Melbourne, pages 61-71, 1994. Superseded by  [102]. (Gzipped PostScript, 11 pages, 67509 bytes)

[104]
L. Birkedal and M. Welinder. Handwriting program generator generators. In Manuel Hermenegildo and Jaan Penjam, editors, Programming Language Implementation and Logic Programming. 6th International Symposium, PLILP '94, volume 844 of Lecture Notes in Computer Science, pages 198-214, Madrid, Spain, September 1994. Springer. (Gzipped PostScript, 17 pages, 54917 bytes)

[105]
L. Birkedal and M. Welinder. Partial evaluation of Standard ML. Technical Report 93/22, DIKU, Department of Computer Science, University of Copenhagen, October 1993. Master's Thesis. (173 pages). (Gzipped PostScript, 175 pages, 307980 bytes)

[106]
L. Birkedal. Higher-order functors and principal signatures in Standard ML. TOPPS Report D-184 (117 pages), September 1993. (Gzipped PostScript, 121 pages, 224682 bytes)

[107]
L. Birkedal and N.J. Rehof. Towards a semantic foundation for binding time analysis. DIKU Student Project, April 1993.