%%% ====================================================================
%%%  BibTeX-file{
%%%	author          = "Lars Birkedal",
%%%	date            = "29 March 2005",
%%%	filename        = "BirkedalL.bib",
%%%     url             = "http://www.itu.dk/people/birkedal/papers/BirkedalL.bib",
%%%     www-home        = "http://www.itu.dk/people/birkedal/",
%%%	address         = "The IT University of Copenhagen,
%%%		           Rued Langgaards Vej 7, DK-2300 Koebenhavn S, 
%%%                        Denmark.",
%%%	email		= "birkedal at itu.dk",
%%%	telephone       = "+45 7218 5280",
%%%	FAX             = "+45 7218 5001",
%%%     dates           = {1990--},
%%%     keywords        = "",
%%%	supported       = "yes",
%%%	supported-by	= "Lars Birkedal",
%%%	abstract        = "Bibliography for Lars Birkedal"
%%%  }
%%% ====================================================================


                  

@InProceedings{BirkedalL:joins-conf,
  author = 	 {K. Svendsen and L. Birkedal and M. Parkinson},
  title = 	 {Joined-up Thinking: A Specification of the Joins Library in Higher-Order Separation Logic},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTbooktitle = {},
  OPTpages = 	 {},
  year =	 {2011},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month =	 apr,
  OPTorganization = {},
  OPTpublisher = {},
  note =	 {Submitted for publication},
  OPTannote = 	 {},
  pdf = {joins-conf.pdf}
}

@Article{Birkedal:step-nondet-journal,
  author = 	 {J. Schwinghammer and L. Birkedal},
  title = 	 {Step-Indexed Relational Reasoning for Countable Nondeterminism},
  journal = 	 {},
  year = 	 {2012},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  month =	 feb,
  note =	 {Submitted for publication (journal version of CSL'11 paper)},
  OPTannote = 	 {},
  pdf = {step-nondet-journal.pdf}
}


@InProceedings{BirkedalL:charge-conf,
  author = 	 {J. Bengtson and J.B. Jensen and L. Birkedal},
  title = 	 {Charge! A Framework for Higher-Order Separation Logic in {Coq}},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTbooktitle = {ITP},
  OPTpages = 	 {},
  year =	 {2012},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month =	 feb,
  OPTorganization = {},
  OPTpublisher = {},
  note =	 {To Appear (accepted for publication)},
  OPTannote = 	 {},
  pdf = {charge-conf.pdf}
}

@InProceedings{BirkedalL:views,
  author = 	 {T. Dinsdale-Young and L. Birkedal and P. Gardner and M. Parkinson and H. Yang},
  title = 	 {Views: Compositional Reasoning for Concurrency},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTbooktitle = {},
  OPTpages =	 {},
  year =	 {2012},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month =	 jan,
  OPTorganization = {},
  OPTpublisher = {},
  note =	 {Submitted for publication.},
  OPTannote = 	 {},
  pdf = {views.pdf}
}

@InProceedings{BirkedalL:relconc,
  author = 	 {L. Birkedal and F. Sieczkowski and J. Thamsborg},
  title = 	 {A Concurrent Logical Relation},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTbooktitle = {},
  OPTpages = 	 {},
  year =	 {2012},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month =	 jan,
  OPTorganization = {},
  OPTpublisher = {},
  note =	 {Submitted for publication.},
  OPTannote = 	 {},
  pdf = {relconc.pdf}
}

                  
                  
@Article{BirekdalL:relrmhoadt,
  author = 	 {L. Birkedal and K. St{\o}vring and J. Thamsborg},
  title = 	 {A Relational Realizability Model for Higher-Order Stateful {ADT}s},
  journal = 	 {Journal of Logic and Algebraic Programming},
  year = 	 {2012},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  month = 	 jan,
  note = 	 {Accepted for publication},
  OPTannote = 	 {},
  pdf =          {relrmhoadt.pdf}
}
                  

@Article{BirkedalL:sgdt-journal,
  author = 	 {L. Birkedal and R. M{\o}gelberg and J. Schwinghammer and K. St{\o}vring},
  title = 	 {First steps in synthetic guarded domain theory: step-indexing in the topos of trees},
  journal = 	 {},
  year = 	 {2011},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  month =	 {dec},
  note =	 {Submitted for publication (journal version of LICS'11 paper)},
  OPTannote = 	 {},
  pdf = {sgdt-journal.pdf}
}

                  @Article{BirkedalL:stslr-journal,
  author = 	 {D. Dreyer and G. Neis and L. Birkedal},
  title = 	 {The Impact of Higher-Order State and Control Effects on Local Relational Reasoning},
  journal = 	 {Journal of Functional Programming},
  year = 	 {2012},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  month = 	 feb,
  note = 	 {To Appear (accepted for publication).},
  OPTannote = 	 {},
  pdf =          {stslr-journal.pdf}
}
                  

                  
@Article{BirkedalL:antiframe-long,
  author = 	 {J. Schwinghammer and L. Birkedal and F. Pottier and B. Reus and K. St{\o}vring and H. Yang},
  title = 	 {A Step-Indexed {K}ripke Model of Hidden State},
  journal = 	 {Mathematical Structures in Computer Science},
  year = 	 2012,
  note = 	 {(To Appear. Accepted for publication)},
  pdf = {antiframe-long.pdf}
}

@InProceedings{BirkedalL:sharing-conf,
  author = 	 {J.B. Jensen and L. Birkedal},
  title = 	 {Fictional Separation Logic},
  booktitle = {Proceedings of ESOP 2012},
  year = 	 2012,
  pdf =  {sharing-conf.pdf}
}
                  
                  

@InProceedings{BirkedalL:snapshots-conf,
  author = 	 {H. Mehnert and F. Sieczkowski and L. Birkedal and P. Sestoft},
  title = 	 {Formalized Verification of Snapshotable Trees: Separation and Sharing},
  booktitle = {Proceedings of VSTTE 2012},
  year = 	 2012,
  pdf =  {snapshots-conf.pdf}
}

                  

@Article{BirkedalL:bpl-matching-journal,
  author = 	 {T.C. Damgaard and A.J. Glenstrup and L. Birkedal and R. Milner},
  title = 	 {An Inductive Characterization of Matching in Binding Bigraphs},
  journal = 	 {},
  year = 	 {2011},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  OPTmonth = 	 {},
  note = 	 {To Appear in Formal Aspects of Computing (Accepted for publication)},
  OPTannote = 	 {},
  pdf =          {matching-bbg.pdf}
}

                  
@InProceedings{BirkedalL:step-nondet,
  author = 	 {J. Schwinghammer and L. Birkedal},
  title = 	 {Step-Indexed Relational Reasoning for Countable Nondeterminism},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle =	 {Proceedings of CSL},
  OPTpages = 	 {},
  year = 	 {2011},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month = 	 apr,
  OPTorganization = {},
  OPTpublisher = {},
  OPTannote = 	 {},
  pdf = {step-nondet.pdf}
}

@InProceedings{BirkedalL:storable-locks,
  author = 	 {A. Buisse and L. Birkedal and K. St{\o}vring},
  title = 	 {A Step-Indexed Kripke Model of Separation Logic for Storable Locks},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {Proceedings of MFPS},
  OPTpages = 	 {},
  year =	 2011,
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 apr,
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {},
  pdf = {locks.pdf}
}

@InProceedings{BirkedalL:effects,
  author = 	 {J. Thamsborg and L. Birkedal},
  title = 	 {A {K}ripke Logical Relation for Effect-Based Program Transformations},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle =	 {Proceedings of ICFP},
  OPTpages = 	 {},
  year = 	 {2011},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month = 	 mar,
  OPTorganization = {},
  OPTpublisher = {},
  OPTannote = 	 {},
  pdf = {effects.pdf}
}


@Article{BirkedalL:nested-triples-journal,
  author = 	 {J. Schwinghammer and L. Birkedal and B. Reus and H. Yang},
  title = 	 {Nested {H}oare Triples and Frame Rules for Higher-order Store},
  year =	 2011,
  month =	 jul,
  journal = {Logical Methods in Computer Science},
  volume = 7,
  number = {3:21},
  pdf =          {nested-long.pdf}
}
                  

                  
                  @InProceedings{BirkedalL:veroop-conf,
  author = 	 {J. Bengtson and J.B. Jensen and F. Sieczkowski and L. Birkedal},
  title = 	 {Verifying object-oriented programs with higher-order separation logic in {Coq}},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle =	 {Proceedings of ITP},
  OPTpages = 	 {},
  year = 	 {2011},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month = 	 feb,
  OPTorganization = {},
  OPTpublisher = {},
  OPTannote = 	 {},
  pdf = {veroop-conf.pdf}
}

@InProceedings{BirkedalL:parsdtt-conf,
  author = 	 {K. Svendsen and L. Birkedal and A. Nanevski},
  title = 	 {Partiality, State, and Dependent Types},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle =	 {Proceedings of TLCA},
  OPTpages = 	 {},
  year =	 2011,
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month =	 feb,
  OPTorganization = {},
  OPTpublisher = {},
  OPTannote = 	 {},
  pdf = {parsdtt-conf.pdf}
}

@InProceedings{BirkedalL:sgdt-conf,
  author = 	 {L. Birkedal and R. M{\o}gelberg and J. Schwinghammer and K. St{\o}vring},
  title = 	 {First steps in synthetic guarded domain theory: step-indexing in the topos of trees},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle =	 {Proceedings of LICS},
  OPTpages = 	 {},
  year = 	 {2011},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month = 	 jan,
  OPTorganization = {},
  OPTpublisher = {},
  OPTannote = 	 {},
  pdf = {sgdt-conf.pdf}
}

                  @Article{BirkedalL:lsrl-journal,
  author = 	 {D. Dreyer and A. Ahmed and L. Birkedal},
  title = 	 {Logical Step-Indexed Logical Relations},
  journal = 	 {Logical Methods in Computer Science},
  year = 	 2011,
  volume = 	 7,
  number = 	 {2:16},
  month =	 jun,
  pdf = {lslr-journal.pdf}
}


@Misc{BirkedalL:dagstuhl-2010,
  author = 	 {A. Ahmed and N. Benton and L. Birkedal and M. Hofmann},
  title =	 {<a href="http://drops.dagstuhl.de/portals/index.php?semnr=10351">{M}odelling, {C}ontrolling, and {R}easoning about {S}tate</a>},
  howpublished = {Seminar Proceedings, Executive Summary and Abstracts Collection. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany 2010.},
  year =	 2010
}
                  

@InProceedings{BirkedalL:relpoms-antiframe-conf,
  author = 	 {J. Schwinghammer and L. Birkedal and K. St{\o}vring},
  title = 	 {A Step-indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle =	 {Proceedings of FOSSACS 2011},
  OPTpages = 	 {},
  year =	 {2011},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month =	 oct,
  OPTorganization = {},
  OPTpublisher = {},
  OPTannote = 	 {},
  pdf = {relpoms-antiframe-conf.pdf}
}

@InProceedings{BirkedalL:step-recworld-conf,
  author = 	 {L. Birkedal and B. Reus and J. Schwinghammer and K. St{\o}vring and J. Thamsborg and H. Yang},
  title = 	 {Step-Indexed Kripke Models over Recursive Worlds},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle =	 {Proceedings of POPL 2011},
  OPTpages = 	 {},
  year =	 {2011},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTannote = 	 {},
  pdf = {step-recworld-conf.pdf}
}
                  
@Article{BirkedalL:metric-enriched-journal,
                    author = 	 {L. Birkedal and K. St{\o}vring and J. Thamsborg},
  title = 	 {The Category-Theoretic Solution of Recursive Metric-Space Quations},
  journal = 	 {Theoretical Computer Science},
  year = 	 2010,
  volume = 	 411,
  pages = 	 {4102--4122},
  pdf = {metric-enriched-journal.pdf}
}

@Article{BirkedalL:formalizing-semantics,
  author = 	 {N. Benton and L. Birkedal and A. Kennedy and C. Varming},
  title = 	 {Formalizing Domains, Ultrametric Spaces and Semantics of Programming Languages},
  journal = 	 {},
  year = 	 {2010},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  OPTmonth = 	 {},
  note =	 {Submitted for publication. Coq Script: \texttt{<a href="domultracoq.zip">domultracoq.zip </a>}}, 
  pdf =          {formalizing-semantics.pdf}
}

                  
@InProceedings{BirkedalL:relpoms-monotonicity-conf,
  author = 	 {L. Birkedal and J. Schwinghammer and K. St{\o}vring},
  title = 	 {A Step-indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTbooktitle = {},
  OPTpages = 	 {},
  year =	 {2010},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  note =	 {Presented at FICS 2010},
  OPTannote = 	 {},
  pdf = {relpoms-monotonicity-conf.pdf}
}

@InProceedings{BirkedalL:nakano-conf,
  author = 	 {L. Birkedal and J. Schwinghammer and K. St{\o}vring},
  title = 	 {A Metric Model of Guarded Recursion},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTbooktitle = {},
  OPTpages = 	 {},
  year =	 {2010},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTannote = 	 {},
  note = {Presented at FICS 2010},
  pdf = {nakano-conf.pdf}
}

@article{BirkedalL:parametricity-state-metric-journal,
  author = 	 {L. Birkedal and K. St{\o}vring and J. Thamsborg},
  title = 	 {Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types},
  journal = 	 {Mathematical Structures in Computer Science},
  year = 	 2010,
  month = 	 may,
  note = 	 {To Appear (accepted for publication)},
  pdf =          {parametricity-state-metric-journal.pdf}
}
                  
@InProceedings{BirkedalL:stslr-conf,
  author = 	 {D. Dreyer and G. Neis and L. Birkedal},
  title = 	 {The Impact of Higher-Order State and Control Effects on Local Relational Reasoning},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {Proc. of ICFP 2010},
  OPTpages = 	 {},
  year =	 {2010},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  pdf =	 {stslr-conf.pdf}
}


                  
                  
@InProceedings{BirkedalL:views,
  author = 	 {J.B. Jensen and L. Birkedal and P. Sestoft },
  title = 	 {Modular Verification of Linked Lists with Views via Separation Logic},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTbooktitle = {Proc. of FTfJP'2010},
  OPTpages = 	 {},
  year =	 {2010},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTannote = 	 {},
  note = {Presented at FTfJP'2010},
  pdf = {views.pdf}
}





@InCollection{BirkedalL:relational-lifting,
  author = 	 {J. Thamsborg and L. Birkedal and H. Yang},
  title = 	 {Two for the Price of One: Lifting Separation Logic Assertions},
  booktitle = 	 {},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {},
  OPTpublisher = {},
  year =	 {2010},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTtype = 	 {},
  OPTchapter = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  month =	 jan,
  note =	 {Manuscript},
  OPTannote = 	 {},
  pdf = {relational-lifting.pdf}
}


@InProceedings{BirkedalL:vergd-conf,
  author = 	 {K. Svendsen and L. Birkedal and M. Parkinson},
  title = 	 {Verifying Generics and Delegates},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTbooktitle = {},
  OPTpages = 	 {},
  year =	 {2009},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month =	 dec,
  OPTorganization = {},
  OPTpublisher = {},
  note =         {Accepted for publication in ECOOP 2010},
  pdf =	 {vergd-conf.pdf},
  OPTannote = 	 {}
}
                  
@TechReport{BirkedalL:parametricity-state-metric-tr,
  author = 	 {L. Birkedal and K. St{\o}vring and J. Thamsborg},
  title = 	 {Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types},
  institution =  {IT University of Copenhagen},
  year = 	 2010,
  number =	 {TR-2010-124},
  month =	 {jan},
  pdf =          {ITU-TR-2010-124.pdf}
}

@InProceedings{BirkedalL:infohiding-conf,
  author = 	 {J. Schwinghammer and H. Yang and L. Birkedal and F. Pottier and B. Reus},
  title = 	 {A Semantic Foundation for Hidden State},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {Proceedings of FOSSACS 2010},
  OPTpages = 	 {},
  year =	 {2009},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month =	 oct,
  OPTorganization = {},
  OPTpublisher = {},
  note =	 {To Appear (accepted for publication)},
  OPTannote = 	 {},
  pdf =          {infohiding-conf.pdf}
}

@InProceedings{BirkedalL:ramified-frames-conf,
  author = 	 {N. Krishnaswami and L. Birkedal and J. Aldrich},
  title = 	 {Verifying Event-Driven Programs using Ramified Frame Properties},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle =	 {Proceedings of TLDI'2010},
  OPTpages = 	 {},
  year =	 {2010},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  note =	 {To Appear},
  OPTannote = 	 {},
  pdf =          {ramified-frames.pdf}
}


@TechReport{BirkedalL:metric-enriched-tr,
  author = 	 {L. Birkedal and K. St{\o}vring and J. Thamsborg},
  title = 	 {The Category-Theoretic Solution of Recursive Metric-Space Quations},
  institution =  {IT University of Copenhagen},
  year = 	 2009,
  number = 	 {ITU-2009-119},
  pdf = 	 {ITU-TR-2009-119.pdf}}

@InProceedings{BirkedalL:ladr-conf,
  author = 	 {D. Dreyer and G. Neis and A. Rossberg and L. Birkedal},
  title = 	 {A Relational Modal Logic for Higher-order Stateful {ADT}s},
  booktitle =	 {Proceedings of POPL'2010},
  year =	 2010,
  month =	 jan,
  pdf =          {ladr-conf.pdf}
}

@InProceedings{BirkedalL:metric-enriched-conf,
  author = 	 {L. Birkedal and K. St{\o}vring and J. Thamsborg},
  title = 	 {Solutions of Generalized Recursive Metric-Space Equations},
  booktitle =	 {Proceedings of FICS 2009},
  year =	 2009,
  month =	 sep,
  pdf =          {metric-enriched-conf.pdf}
}

@InProceedings{BirkedalL:lslr-conf,
  author = 	 {D. Dreyer and A. Ahmed and L. Birkedal},
  title = 	 {Logical Step-Indexed Logical Relations},
  booktitle =	 {Proceedings of LICS 2009},
  year =	 2009,
  month =	 aug,
  pdf =          {lslr-conf.pdf}
}

@InProceedings{BirkedalL:nested-triples-conf,
  author = 	 {J. Schwinghammer and L. Birkedal and B. Reus and H. Yang},
  title = 	 {Nested {H}oare Triples and Frame Rules for Higher-order Store},
  booktitle =	 {Proceedings of CSL 2009},
  year =	 2009,
  month =	 apr,
  pdf =          {nested-triples-conf.pdf}
}


                  

@TechReport{BirkedalL:bpl-higherorder-tr,
  author = 	 {L. Birkedal and M. Bundgaard and S. Debois and T. Hildebrandt and D. Grohmann},
  title = 	 {Higher-order Contexts via Games and the {I}nt-Construction},
  institution =  {IT University of Copenhagen},
  year = 	 2009,
  number = 	 {ITU-TR-2009-117},
  pdf =          {ITU-TR-2009-117.pdf}
}

@InProceedings{BirkedalL:parametricity-state-metric-conf,
  author = 	 {L. Birkedal and K. St{\o}vring and J. Thamsborg},
  title = 	 {Realizability Semantics of Parametric Polymorphism, References, and Recursive Types},
  booktitle =    {Proceedings of FOSSACS'09},
  year = 	 2009,
  month = 	 apr,
  pdf = {parametricity-state-metric-conf.pdf}
}

@InProceedings{BirkedalL:poswsr,
  author = 	 {L. Birkedal and K. St{\o}vring and J. Thamsborg},
  title = 	 {Relational Parametricity for References and Recursive Types},
  booktitle =    {Proceedings of TLDI},
  year = 	 2009,
  month = 	 jan,
  pdf = {poswsr-conf.pdf}
}

@InProceedings{BirkedalL:design-patterns-conf,
  author = 	 {N. Krishnaswami and J. Aldrich and L. Birkedal and K. Svendsen and A. Buisse},
  title = 	 {Design Patterns in Separation Logic},
  booktitle = {Proc. of TLDI 2009},
  year = 	 2009,
  month = 	 jan,
  pdf = {design-patterns-conf.pdf}

}

@TechReport{BirkedalL:design-patterns-in-htt-tr,
  author =       {K. Svendsen and A. Buisse and L. Birkedal]},
  title  =       {Verifying Design Patterns in {H}oare Type Theory},
  institution =  {IT University of Copenhagen},
  year =         {2008},
  number =       {ITU-TR-2008-112},
  month =        sep,
  pdf =          {ITU-TR-2008-112.pdf}
}

@InProceedings{BirkedalL:ynot-conf,
  author = 	 {A. Nanevski and G. Morrisett and A. Shinnar and P. Goverau and L. Birkedal},
  title =	 {Ynot: Dependent Types for Imperative Programs},
  booktitle = {Proc. of ICFP 2008},
  month =	 {Sep},
  year =	 2008,
  pdf =          {ynot-conf.pdf}
}

@InProceedings{BirkedalL:suppsort,
  author = 	 {L. Birkedal and S. Debois and T. Hildebrandt},
  title =	 {On the Construction of Sorted Bigraphical Reactive Systems},
  booktitle = {Proc. of CONCUR 2008},
  month =	 {Sep},
  year =	 2008,
  pdf =          {suppsort.pdf}
}


@Article{BirkedalL:lapl-struct-journal,
  author = 	 {L. Birkedal and R.E. M{\o}gelberg and R.L. Petersen},
  title = 	 {Category-theoretic Models of {L}inear {A}badi \& {P}lotkin {L}ogic},
  journal = 	 {Theory and Applications in Categories},
  year = 	 2008,
  volume =	 20,
  number =	 7,
  pages =	 {116--151},
  pdf = {http://www.tac.mta.ca/tac/volumes/20/7/20-07.pdf}
}


@Article{BirkedalL:sdt-lapl-journal,
  author = 	 {R.E. M{\o}gelberg and L. Birkedal and G. Rosolini},
  title = 	 {Synthetic Domain Theory and Models of {L}inear {A}badi \& {P}lotkin {L}ogic},
  journal = 	 {Annals of Pure and Applied Logic},
  year = 	 {2008},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {To Appear (accepted for publication)},
  OPTannote = 	 {},
  pdf = {sdt-lapl-journal.pdf}
}

@InProceedings{BirkedalL:seplhostore-conf,
  author = {L. Birkedal and B. Reus and J. Schwinghammer and H. Yang},
  title =  {A {S}imple {M}odel of {S}eparation {L}ogic for {H}igher-order {S}tore},
  booktitle = {Proceedings of ICALP 2008},
  year = 2008,
  notes = {To Appear at ICALP 2008 (accepted for publication)},
  pdf = {seplhostore-conf.pdf}
}



@InProceedings{BirkedalL:hosl-formalization,
  author = 	 {C. Varming and L. Birkedal},
  title = 	 {Higher-Order Separation Logic in {I}sabelle/{HOLCF}},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle =	 {Proceedings of MFPS 2008},
  OPTpages = 	 {},
  year =	 {2008},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {(accepted for publication)},
  OPTannote = 	 {},
  pdf = {hosl-formalization.pdf}
}

@Article{BirkedalL:parsepl-journal,
  author = 	 {L. Birkedal and H. Yang},
  title = 	 {Relational Parametricity and Separation Logic},
  journal = 	 {Logical Methods in Computer Science},
  year = 	 {2008},
  OPTkey = 	 {},
  volume =	 {4},
  number =	 {2:6},
  pages =	 {1--27},
  OPTmonth = 	 {},
  note =         {<a href="http://lmcs-online.org/ojs/viewarticle.php?id=358&layout=abstract">lmcs online version</a>},
  pdf =          {parsepl-lmcs.pdf}
}


@InProceedings{BirkedalL:httmodel-conf,
  author = {R.L. Petersen and L. Birkedal and A. Nanevski and G. Morrisett},
  title =  {A {R}ealizability {M}odel of {I}mpredicative {H}oare {T}ype {T}heory},
  booktitle = {Proceedings of ESOP 2008},
  year = 2008,
  pdf = {HTTmodel-conf.pdf}
}

@Article{BirkedalL:lapl-permodel-journal,
  author = 	 {L. Birkedal and R.E. M{\o}gelberg and R.L. Petersen},
  title = 	 {Domain-theoretic Models of Parametric Polymorphism},
  journal = 	 {Theoretical Computer Science},
  year = 	 2007,
  volume =	 388,
  number =	 {1--3},
  pages =	 {152--172},
  pdf = {lapl-permodel-journal.pdf}
}

@Article{BirkedalL:bpl-implmatch,
  author = 	 {A.J. Glenstrup and T.C. Damgaard and L. Birkedal and E. H{\o}jsgaard},
  title = 	 {An Implementation of Bigraph Matching},
  journal = 	 {},
  year = 	 {2007},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  OPTmonth = 	 {},
  note = 	 {Submitted for publication},
  OPTannote = 	 {},
  pdf =          {implmatch.pdf}
}




@Article{BirkedalL:polshtt-journal,
  author = 	 {A. Nanevski and G. Morrisett and L. Birkedal},
  title = 	 {Hoare Type Theory, Polymorphism and Separation},
  journal = 	 {Journal of Functional Programming},
  year = 	 {2007},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  OPTmonth = 	 {},
  note = 	 {To Appear (accepted for publication)},
  OPTannote = 	 {},
  pdf =          {polshtt-journal.pdf}
}

@TechReport{BirkedalL:httmodel-tr,
  author = {R.L. Petersen and L. Birkedal and A. Nanevski and G. Morrisett},
  title =  {A {R}ealizability {M}odel of {I}mpredicative {H}oare {T}ype {T}heory},
  institution = {IT University of Copenhagen},
  year = 2007,
  pdf = {HTTmodel-tr.pdf}
}

@InProceedings{BirkedalL:subject-observers-conf,
  author = {N. Krishnaswami and J. Aldrich and L. Birkedal},
  title =  {Modular Verification of the Subject-Observer Pattern via Higher-order Separation Logic},
  booktitle = {9th Workshop on Formal Techniques for Java-like Programs (FTfJP 2007)},
  year =   2007,
  pdf = {BirkedalL:subject-observers-conf.pdf}
}

@Article{BirkedalL:hosl-bihyp-journal,
  author = 	 {B. Biering and L. Birkedal and N. Torp-Smith},
  title = 	 {{BI}-Hyperdoctrines, Higher-order Separation Logic, and Abstraction},
  journal = 	 {ACM Transactions on Programming Languages and Systems},
  year = 	 {2007},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  OPTmonth = 	 {},
  note = 	 {To appear},
  OPTannote = 	 {},
  pdf =          {hosl-journal.pdf}
}

@InProceedings{BirkedalL:bpl-matching-conf,
  author =	 {L. Birkedal and T.C. Damgaard and A. Glenstrup and R. Milner},
  title =	 {Matching of Bigraphs},
  booktitle =    {Proceedings of Graph Transformation for Verification and Concurrency 2006}, 
  year =         2007,
  month =        {Jan},
  pdf =          {bpl-matching-conf.pdf}
}

@InProceedings{BirkedalL:parsepl-conf,
  author =       {L. Birkedal and H. Yang},
  title =        {Relational Parametricity and Separation Logic},
  year =         2007,
  booktitle =    {Proceedings of FOSSACS 2007},
  pdf =          {parsepl-conf.pdf}
}

@InProceedings{BirkedalL:abspmd-conf,
  author =       {A. Nanevski and A. Ahmed and G. Morrisett and L. Birkedal},
  title =        {Abstract Predicates and Mutable {ADT}s in {H}oare Type Theory},
  year =         2007,
  booktitle =    {Proceedings of ESOP 2007},
  pdf =          {abspmd-conf.pdf}
}


@Article{BirkedalL:lapl-journal,
  author = 	 {L. Birkedal and R.E. M{\o}gelberg and R.L. Petersen},
  title = 	 {Linear {A}badi and {P}lotkin Logic},
  journal =      {Logical Methods in Computer Science},
  volume =          {2},
  number =       {5:2},
  year = 	 2006,
  month = 	 aug,
  note =         {<a href="http://lmcs-online.org/ojs/viewarticle.php?id=179&layout=abstract">lmcs online version</a>}
}




@TechReport{BirkedalL:abspmd-tr,
  author =       {A. Nanevski and A. Ahmed and G. Morrisett and L. Birkedal},
  title =        {Abstract Predicates and Mutable {ADT}s in {H}oare Type Theory},
  institution =  {Harvard University},
  year =         2006,
  number =       {TR--14--06},
  month =        {September},
  pdf =          {abspmd-tr.pdf}
}

@Article{BirkedalL:semslt-lmcs,
  author = 	 {L. Birkedal and N. Torp-Smith and H. Yang},
  title = 	 {Semantics of Separation-logic Typing and Higher-order Frame Rules for Algol-like Languages},
  journal =      {Logical Methods in Computer Science},
  volume =          {2},
  number =       {5:1},
  year = 	 2006,
  month = 	 aug,
  note =         {<a href="http://lmcs-online.org/ojs/viewarticle.php?id=149&layout=abstract">lmcs online version</a>}
}


@Article{BirkedalL:locrcg-journal,
  author = 	 {N. Torp-Smith and L. Birkedal and J.C. Reynolds},
  title = 	 {Local Reasoning about a Copying Garbage Collector},
  journal =      {ACM Transactions on Programming Languages and Systems},
  year =	 2006,
  publisher =	 {ACM Press},
  note =         {To Appear},
  pdf =   {locrcg.pdf}
}


@InProceedings{BirkedalL:polshtt-conf,
  author =       {A. Nanevski and G. Morrisett and L. Birkedal},
  title =        {Polymorphism and Separation in Hoare Type Theory},
  booktitle =    {Proceedings of ICFP 2006},
  editor =       {Julia Lawall},
  year =         2006,
  OPTvolume =    {},
  month =        sep,
  note =         {To appear},
  pdf =          {icfp06.pdf}
}


@InProceedings{BirkedalL:sorrs-conf,
  author =       {L. Birkedal and S. Debois and T. Hildebrandt},
  title =        {Sortings for Reactive Systems},
  booktitle =    {Proceedings of CONCUR 2006},
  editor =       {Christel Baier and Holger Hermanns},
  year =         2006,
  OPTvolume =    {},
  month =        aug,
  pdf =          {sorrs-conf.pdf}
}


@InProceedings{BirkedalL:relrrtr-conf,
  author =       {N. Bohr and L. Birkedal},
  title =        {Relational Reasoning for Recursive Types and References},
  booktitle =    {Proceedings of APLAS 2006},
  year =         2006,
  month =        {June},
  pdf =          {relrrtr.pdf}
}

@InProceedings{BirkedalL:lily-lapl-conf,
  author =       {L. Birkedal and R.L. Petersen and R. M{\o}gelberg and C. Varming},
  title =        {Operational Semantics and Models of {L}inear {A}badi \& {P}lotkin {L}ogic},
  booktitle =    {},
  year =         2006,
  month =        {June},
  note =         {Submitted for publication},
  pdf =          {lily-lapl-conf.pdf}
}

@TechReport{BirkedalL:bpl-matching-tr,
  author =	 {L. Birkedal and T.C. Damgaard and A. Glenstrup and R. Milner},
  title =	 {Matching of Bigraphs},
  institution =  {IT University of Copenhagen},
  year =         2006,
  number =       {ITU-TR-2006-88},
  month =        {June},
  pdf =          {ITU-TR-2006-88.pdf}
}


@TechReport{BirkedalL:polshtt-tr,
  author =       {A. Nanevski and G. Morrisett and L. Birkedal},
  title =        {Polymorphism and Separation in Hoare Type Theory},
  institution =  {Harvard University},
  year =         2006,
  number =       {TT--10--06},
  month =        {April},
  pdf =          {polshtt-tr.pdf}
}


@Article{BirkedalL:axb,
  author =       {T.C. Damgaard and L. Birkedal},
  title =        {Axiomatizing Binding Bigraphs},
  journal =      {Nordic Journal of Computing},
  year =         {2006},
  volume =       13,
  number =       {1-2},
  pages =        {58--77},
  pdf =          {axb-njc.pdf}
}


@TechReport{BirkedalL:sorrs-tr,
  author =       {L. Birkedal and S. Debois and T. Hildebrandt},
  title =        {Sortings for Reactive Systems},
  institution =  {IT University of Copenhagen},
  year =         2006,
  number =       84,
  address =      {Rued Langgards Vej 7, DK-2300 Copenhagen V},
  month =        {March},
  pdf =          {ITU-TR-2006-84.pdf}
}



@Misc{BirkedalL:bigplpc,
  author = 	 {L. Birkedal and M. Bundgaard and T.C. Damgaard and S. Debois and E. Elsborg and A.J. Glenstrup and T. Hildebrandt and R. Milner and H. Niss},
  title =	 {Bigraphical Programming Langauges for Pervasive Computing},
  howpublished = {In International Workshop on Combining Theory and Systems Building in Pervasive Computing. Position Paper.},
  month =	 {May},
  year =	 2006,
  pdf =          {bigplpc.pdf}
}


@InProceedings{BirkedalL:bigmcs-conf,
  author =       {L. Birkedal and S. Debois and E. Elsborg and T. Hildebrandt and H. Niss},
  title =        {Bigraphical {M}odels of {C}ontext-aware {S}ystems},
  booktitle =    {Foundations of Software Science and Computation Structures (FOSSACS) 2006},
  year =         2006,
  series = 	 {Lecture Notes in Computer Science},
  number =       3921,
  month =        {March},
  pdf =          {bigmcs-conf.pdf}
}


@TechReport{BirkedalL:bigmcs-tr,
  author =       {L. Birkedal and S. Debois and E. Elsborg and T. Hildebrandt and H. Niss},
  title =        {Bigraphical {M}odels of {C}ontext-aware {S}ystems},
  institution =  {IT University of Copenhagen},
  year =         2005,
  number =       74,
  address =      {Rued Langgards Vej 7, DK-2300 Copenhagen V},
  month =        {November},
  note =         {ISBN: 87-7949-110-3},
  pdf =          {ITU-TR-2005-74.pdf}
}



@TechReport{BirkedalL:axibb-tr-revised,
  author = 	 {T.C. Damgaard and L. Birkedal},
  title = 	 {Axiomatizing Binding Bigraphs (revised)},
  institution =  {IT University of Copenhagen},
  year = 	 2005,
  number =	 {TR-2005-71},
  month =	 mar,
  note =	 {36 pages},
  pdf =          {ITU-TR-2005-71.pdf}
}


@TechReport{BirkedalL:hosl-bihyp-tr,
  author =       {B. Biering and L. Birkedal and N. Torp-Smith},
  title =        {{BI}-Hyperdoctrines, Higher-order Separation Logic, and Abstra
ction},
  institution =  {IT University of Copenhagen},
  year =         {2005},
  number =	 {ITU-TR-2005-69},
  month =     jul,
  pdf =          {ITU-TR-2005-69.pdf}
}

@TechReport{BirkedalL:axibb-tr,
  author = 	 {T.C. Damgaard and L. Birkedal},
  title = 	 {Axiomatizing Binding Bigraphs},
  institution =  {IT University of Copenhagen},
  year = 	 2005,
  number =	 {TR-2005-65},
  month =	 mar,
  note =	 {37 pages},
  postscript =   {axibb-tr.ps.gz},
  pdf =          {axibb-tr.pdf}
}

@Article{BirkedalL:catmap,
  author = 	 {L. Birkedal and R.E. M{\o}gelberg},
  title = 	 {Categorical Models of {Abadi-Plotkin's} Logic for Parametricity},
  journal = 	 {Mathematical Structures in Computer Science},
  year = 	 2005,
  volume =	 15,
  pages =	 {709-772},
  pdf =          {catmap.pdf},
  postscript =   {catmap.ps.gz}
}

@InProceedings{BirkedalL:hosl,
  author = 	 {L. Birkedal and N. Torp-Smith},
  title = 	 {Higher-order Separation Logic and Abstraction},
  booktitle = 	 {},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {},
  year =	 {2005},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month =	 feb,
  OPTorganization = {},
  OPTpublisher = {},
  note = 	 {Manuscript},
  OPTannote = 	 {},
  postscript =   {hosl.ps.gz}
}

@InProceedings{BirkedalL:lapl-mfps,
  author = 	 {L. Birkedal and R.E. M{\o}gelberg and R.L. Petersen},
  title = 	 {Parametric Domain-theoretic Models of Polymorphic Intuitionistic / Linear Lambda Calculus},
  booktitle = 	 {},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {},
  year =	 {2005},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month =	 feb,
  OPTorganization = {},
  OPTpublisher = {},
  note = 	 {Mathematical Foundations of Programming Semantics 2005},
  OPTannote = 	 {},
  pdf =   {lapl-mfps.pdf}
}

@InProceedings{BirkedalL:sdt-lapl-mfps,
  author = 	 {R.E. M{\o}gelberg and L. Birkedal and G. Rosolini},
  title = 	 {Synthetic Domain Theory and Models of Linear {Abadi} and {Plotkin} Logic},
  booktitle = 	 {},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {},
  year =	 {2005},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month =	 feb,
  OPTorganization = {},
  OPTpublisher = {},
  note = 	 {Mathematical Foundations of Programming Semantics 2005},
  OPTannote = 	 {},
  pdf =   {sdt-lapl-mfps.pdf}
}




@TechReport{BirkedalL:lapl-tr,
  author = 	 {L. Birkedal and R.E. M{\o}gelberg and R.L. Petersen},
  title = 	 {Parametric Domain-Theoretic Models of Linear {Abadi-Plotkin}
Logic},
  institution =  {IT University of Copenhagen},
  year = 	 2005,
  number =	 {TR-2005-57},
  postscript =   {lapl-tr.ps.gz},
  pdf =          {lapl-tr.pdf}
}

@TechReport{BirkedalL:sdt-lapl-tr,
  author = 	 {R.E. M{\o}gelberg and L. Birkedal and G. Rosolini},
  title = 	 {Synthetic Domain Theory and Models of Linear {Abadi} and {Plotkin} Logic},
  institution =  {IT University of Copenhagen},
  year = 	 2005,
  number =	 {TR-2005-59},
  month =	 feb,
  postscript =   {sdt-lapl-tr.ps.gz},
  pdf =          {sdt-lapl-tr.pdf}

}

@TechReport{BirkedalL:catmp,
  author =       {R.E. M{\o}gelberg and L. Birkedal and R.L. Petersen},
  title =        {Categorical models of {PILL}},
  year =         2005,
  month =        {February},
  number =       {TR-2005-58},
  institution =  {IT University of Copenhagen},
  postscript =   {catmp.ps.gz},
  pdf =   {catmp.pdf}
}


@InProceedings{BirkedalL:semslt,
  author = 	 {L. Birkedal and N. Torp-Smith and H. Yang},
  title = 	 {Semantics of Separation-logic Typing and Higher-order Frame Rules},
  booktitle = 	 {Proceedings of the 20th IEEE Symposium of Logic in Computer Science (LICS'05)},
  pages =	 {260--269},
  year = 	 2005,
  address =	 {Chicago, IL, USA},
  month = 	 jun,
  pdf        =   {semslt.pdf}
}

@InProceedings{BirkedalL:bihsl,
  author = 	 {B. Biering and L. Birkedal and N. Torp-Smith},
  title = 	 {BI Hyperdoctrines and Higher-order Separation Logic},
  booktitle =	 {In Proceedings of European Symposium on Programming},
  pages =	 {233-247},
  year =	 2005,
  volume =	 3444,
  series =	 {LNCS},
  pdf =   {bihsl.pdf}
}

@InProceedings{BirkedalL:infcdm,
  author = 	 {J.Aa. S{\o}rensen and K.J. Kristoffersen and A. Cervera and M. Schi{\o}tz and T. Lynge and Z. Safar and L. Birkedal},
  title = 	 {An Infrastructure for Context-dependent Mobile Multimedia Communication},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {Proceedings of 2004 IEEE International Workshop on Multimedia Signal Processing},
  OPTpages = 	 {},
  year =	 {2004},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month =	 sep,
  OPTorganization = {},
  OPTpublisher = {},
  OPTannote = 	 {},
  pdf = {infcdm.pdf}
}

@InProceedings{BirkedalL:lacomoco-bpl,
  author = 	 {L. Birkedal},
  title = 	 {Bigraphical {Programming} {Languages} - A {LaCoMoCo} research project},
  booktitle = 	 {2nd UK-Ubinet Workshop, Cambridge, UK},
  year =	 2004,
  month =	 {May},
  note =	 {Position Paper},
  pdf =          {LaCoMoCo-BPL.pdf}
}

@TechReport{BirkedalL:defp-tr,
  author = 	 {L. Birkedal and R.E. M{\o }gelberg},
  title = 	 {On the Definition of Parametricity},
  institution =  {The IT University of Copenhagen},
  year = 	 2004,
  number =	 44,
  postscript =   {defp-tr.ps.gz}
}



@Article{BirkedalL:regmmp,
  author = 	 {M. Tofte and L. Birkedal and M. Elsman and N. Hallenberg},
  title = 	 {A Retrospective on Region-based Memory Management},
  journal = 	 {Higher Order Symbolic Computation},
  year = 	 {2004},
  volume =	 {17},
  number =	 {2},
  OPTpages = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {},
  postscript =   {regmmp.ps.gz}
}

@InProceedings{BirkedalL:locrcg,
  author = 	 {L. Birkedal and N. Torp-Smith and J.C. Reynolds},
  title = 	 {Local Reasoning about a Copying Garbage Collector},
  booktitle = 	 {Proceedings of the 31-st ACM SIGPLAN-SIGACT 
                  Symposium on Principles of Programming Languages (POPL)},
  year =	 2004,
  month =	 jan,
  pages =        {220--231},
  publisher =	 {ACM Press},
  postscript =   {locrcg.ps.gz}
}

@TechReport{BirkedalL:corgcl,
  author =       {L. Birkedal and N. Torp-Smith and J.C. Reynolds},
  title = 	 {Correctness of a Garbage Collector via Local Reasoning},
  institution =  {The IT University of Copenhagen},
  year = 	 2003,
  number =	 30,
  address =	 {Copenhagen, Denmark},
  month =	 jul,
  postscript =   {corgcl.ps.gz}
}


@Article{BirkedalL:gennr-bsl,
  author = 	 {L.~Birkedal},
  title = 	 {A General Notion of Realizability},
  journal = 	 {Bulletin of Symbolic Logic},
  year = 	 2002,
  volume =	 8,
  number =	 2,
  pages =	 {266-282},
  postscript =   {gennr-bsl.ps.gz}
}


@Manual{BirkedalL:prorml4,
  title = 	 {Programming with Regions in the {ML} {Kit} (for Version 4)},
  author =	 {M. Tofte and L. Birkedal and M. Elsman and
N. Hallenberg and T.H. Olesen and P. Sestoft},
  organization = {The IT University of Copenhagen},
  month =	 Sep,
  year =	 2001,
  note =	 {(234 pages). Available via
\texttt{http://www.it-c.dk/research/mlkit}},
  postscript =   {prorml4.ps.gz}
}

@Article{BirkedalL:relmrr,
  author = 	 {L.~Birkedal and J.~van~Oosten},
  title = 	 {Relative and Modified Relative Realizability},
  journal = 	 {Annals of Pure and Applied Logic},
  year = 	 2002,
  volume =	 118,
  number =	 {1--2},
  pages =	 {115--132},
  postscript =   {relmrr.ps.gz}
}

@Article{BirkedalL:elealm,
  author = 	 {S. Awodey and L. Birkedal},
  title = 	 {Elementary Axioms for Local Maps of Toposes},
  journal = 	 {Journal of Pure and Applied Algebra},
  year = 	 2003,
  volume =	 177,
  number =	 3,
  month =	 feb,
  pages =	 {215--230},
  postscript =   {elealm.ps.gz},
}

@Article{BirkedalL:devttc,
  author = 	 {L.~Birkedal},
  title = 	 {Developing Theories of Types and 
                  Computability via Realizability}, 
  journal = 	 {Electronic Notes in Theoretical Computer Science},
  year = 	 2000,
  volume =	 34,
  note =	 {Available at \texttt{http://www.elsevier.nl/locate/entcs/volume34.html}. The pdf version has active hyperreferences and is therefore the preferred version for reading online.}, 
  pdf =          {devttc.pdf},
  postscript =   {devttc.ps.gz},
}

@TechReport{BirkedalL:relmrr-tr,
  author = 	 {L.~Birkedal and J.~van~Oosten},
  title = 	 {Relative and Modified Relative Realizability},
  institution =  {Department of Mathematics, Universiteit Utrecht},
  year = 	 {2000},
  OPTkey = 	 {},
  type =	 {Preprint},
  number =	 {1146},
  OPTaddress = 	 {},
  month =	 mar,
  note = 	 {Superseded by~\cite{BirkedalL:relmrr}},
  OPTannote = 	 {}
}

@InProceedings{BirkedalL:confdt,
  author = 	 {A.~Bauer and L.~Birkedal},
  title = 	 {Continuous Functionals of Dependent Types and
                  Equilogical Spaces},
  booktitle = 	 {Computer Science Logic, 14th Annual Conference of the EACSL,
                  Fischbachau, Germany, August 21-26, 2000},
  year =	 2000,
  editor =	 {P.~Clote and H. Schwichtenberg},
  volume =	 1862,
  series =	 {Lecture Notes in Computer Science},
  month =	 aug,
  publisher =	 {Springer},
  postscript =   {confdt.ps.gz}
}

@Proceedings{BirkedalL:tutwrs-mscs,
  title = 	 {Tutorial Workshop on  Realizability Semantics, {FLoC'99}, Trento, Italy, 1999. Mathematical Structures in Computer Science},
  year = 	 2002,
  editor =	 {L.~Birkedal and J.~van~Oosten and G.~Rosolini and D.S.~Scott},
  volume =	 12,
  publisher =	 {Cambridge University Press}
}

@Article{BirkedalL:locrtm,
  author = 	 {S.~Awodey and L.~Birkedal and D.S.~Scott},
  title = 	 {Local Realizability Toposes and a Modal Logic 
                  for Computability}, 
  journal = 	 {Mathematical Structures in Computer Science},
  year = 	 2002,
  volume =	 {12},
  number =	 {3},
  pages =	 {319--334},
  postscript =   {locrtm.ps.gz}
}

@PhdThesis{BirkedalL:devttc:phd,
  author = 	 {L.~Birkedal},
  title = 	 {Developing Theories of Types and Computability
                  via Realizability},
  school = 	 {School of Computer Science, Carnegie Mellon University},
  year = 	 1999,
  month =	 dec,
  note =	 {Available as CMU Technical Report: CMU-CS-99-173.
                  Superseded by~\cite{BirkedalL:devttc}},
  postscript =   {}
}

@InProceedings{BirkedalL:gennr,
  author = 	 {L.~Birkedal},
  title = 	 {A General Notion of Realizability},
  booktitle = 	 {Proceedings of the 15th Annual IEEE Symposium 
                  on Logic in Computer Science}, 
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {},
  year =	 2000,
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  organization = {IEEE Computer Society},
  address =	 {Santa Barbara, California},
  month =	 {June},
  OPTpublisher = {},
  note =	 {To Appear},
  OPTannote = 	 {},
  postscript =   {gennr.ps.gz}
}

@TechReport{BirkedalL:elealm:tr,
  author = 	 {S. Awodey and L. Birkedal},
  title = 	 {Elementary Axioms for Local Maps of Toposes},
  institution =  {Department of Philosophy, Carnegie Mellon University},
  year = 	 1999,
  number =	 {CMU--PHIL--103},
  month =	 nov,
  note =	 {Submitted for Publication},
  postscript =   {elealm:tr.ps.gz}
}

@InProceedings{BirkedalL:locrtm:entcs,
  author = 	 {S.~Awodey and L.~Birkedal and D.S.~Scott},
  title = 	 {Local Realizability Toposes and a Modal Logic 
                  for Computability},
  booktitle = 	 {Tutorial Workshop on Realizability Semantics, 
                  {FLoC'99}, Trento, Italy, 1999},
  editor =	 {L. Birkedal and J. van~Oosten and G. Rosolini and D.S. Scott},
  volume =	 23,
  series =	 {Electronic Notes in Theoretical Computer Science},
  year =	 1999,
  publisher =	 {Elsevier},
  note =         {Superseded by~\cite{BirkedalL:locrtm}},
  postscript =   {locrtm:entcs.ps.gz}
}

@TechReport{BirkedalL:locrtm:tr,
  author = 	 {S.~Awodey and L.~Birkedal and D.S.~Scott},
  title = 	 {Local Realizability Toposes and a Modal Logic 
                  for Computability},
  institution =  {Department of Philosophy, Carnegie Mellon University},
  year = 	 1999,
  number =	 {CMU-PHIL-99},
  month =	 apr,
  note =         {Superseded by~\cite{BirkedalL:locrtm}},
  postscript =   {locrtm:entcs.ps.gz}
}

@Article{BirkedalL:equs,
  author = 	 {A.~Bauer and L.~Birkedal and D.S.~Scott},
  title = 	 {Equilogical Spaces},
  journal = 	 {Theoretical Computer Science},
  year = 	 2004,
  volume =	 315,
  number =	 1,
  pages =	 {35--59},
  postscript =   {equs.ps.gz}
}

@InProceedings{BirkedalL:typtec,
  author = 	 {L.~Birkedal and A.~Carboni and G.~Rosolini and D.S.~Scott},
  title = 	 {Type Theory via Exact Categories},
  booktitle = 	 {Proceedings of the 13th Annual IEEE Symposium 
                  on Logic in Computer Science}, 
  year =	 1998,
  organization = {IEEE Computer Society},
  address =	 {Indianapolis, Indiana},
  month =	 {June},
  pages =	 {188--198},
  postscript =   {typtec.ps.gz}
}

@Article{BirkedalL:conirt,
  author = 	 {L.~Birkedal and R.W.~Harper},
  title = 	 {Constructing Interpretations of Recursives Types in 
                  an Operational Setting},
  journal = 	 {Information and Computation},
  year = 	 1999,
  volume =	 155,
  pages =	 {3--63},
  postscript =   {conirt.ps.gz}
}

@TechReport{BirkedalL:conirt:tr,
  author = 	 {L.~Birkedal and R.W.~Harper},
  title = 	 {Constructing Interpretations of Recursives Types in 
                  an Operational Setting},
  institution =  {School of Computer Science, Carnegie Mellon University},
  year = 	 1998,
  number =	 {CMU--CS--98--125},
  month = 	 apr,
  note = 	 {Superseded by~\cite{BirkedalL:conirt}},
  postscript =   {conirt:tr.ps.gz}
}

@InProceedings{BirkedalL:conirt:tacs,
  author = 	 {L.~Birkedal and R.W.~Harper},
  title = 	 {Constructing Interpretations of Recursive Types in 
                  an Operational Setting (Summary)},
  booktitle = 	 {Theoretical Aspects of Computer Software: 
                  International Symposium},
  editor =	 {M. Abadi and I. Takayasu},
  volume =	 1281,
  series =	 {Lecture Notes in Computer Science},
  year =	 1997,
  publisher =	 {Springer},
  address =	 {Sendai, Japan},
  month =	 {September},
  pages =	 {458--490},
  note = 	 {Superseded by~\cite{BirkedalL:conirt}},
  postscript =   {conirt:tacs.ps.gz}
}

@Article{BirkedalL:conria,
  author = 	 {L.~Birkedal and M.~Tofte},
  title = 	 {A Constraint-Based Region Inference Algorithm},
  journal = 	 {Theoretical Computer Science},
  year = 	 2001,
  volume =	 258,
  pages =	 {299-392},
  postscript =   {conria.ps.gz}
}

@Article{BirkedalL:regia,
  author = 	 {M.~Tofte and L.~Birkedal},
  title = 	 {A Region Inference Algorithm},
  journal = 	 {ACM Transactions on Programming Languages and Systems},
  year = 	 1998,
  volume =	 20,
  number =	 4,
  month =	 {July},
  pages =	 {734--767},
  note = 	 {(plus 24 pages of electronic appendix)},
  postscript =   {regia.ps.gz}
}

@Article{BirkedalL:unipri,
  author = 	 {M.~Tofte and L.~Birkedal},
  title = 	 {Unification and Polymorphism in Region Inference},
  journal = 	 {To Appear in Milner Festschrift (Accepted)},
  year = 	 {1998},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTmonth = 	 {},
  OPTpages = 	 {},
  note =	 {(25 pages)},
  OPTannote = 	 {},
  postscript =   {unipri.ps.gz}
}

@InProceedings{BirkedalL:reginm,
  author = 	 {L.~Birkedal and M.~Tofte and M.~Vejlstrup},
  title = 	 {From Region Inference to von {Neumann} 
                  Machines via Region Representation Inference},
  booktitle = 	 {Proceedings of the 23-rd ACM SIGPLAN-SIGACT 
                  Symposium on Principles of Programming Languages (POPL)},
  year =	 1996,
  publisher =	 {ACM Press},
  month =	 jan,
  pages =	 {171--183},
  postscript =   {reginm.ps.gz}
}

@TechReport{BirkedalL:prorml3,
  author = 	 {M.~Tofte and L.~Birkedal and M.~Elsman and
                  N.~Hallenberg and T.H.~Olesen and P.~Sestoft 
                  and P.~Bertelsen},
  title = 	 {Programming with Regions in the {ML} {Kit} (for Version 3)},
  institution =  {Department of Computer Science, University of Copenhagen},
  year = 	 1998,
  number =	 {98/25},
  month = 	 nov,
  note = 	"(214 pages)",
  url =          {http://www.itu.dk/research/mlkit},
  postscript =   {prorml3.ps.gz}
}

@TechReport{BirkedalL:prorml,
  author = 	 {M.~Tofte and L.~Birkedal and M.~Elsman and
                  N.~Hallenberg and T.H.~Olesen and P.~Sestoft 
                  and P.~Bertelsen},
  title = 	 {Programming with Regions in the {ML} {Kit}},
  institution =  {Department of Computer Science, University of Copenhagen},
  year = 	 1997,
  number =	 {97/12},
  note = 	 {(194 pages)},
  url =          {http://www.itu.dk/research/mlkit},
  postscript =   {prorml.ps.gz}
}

@TechReport{BirkedalL:mlkit1,
  author = 	{L.~Birkedal and N.~Rothwell and M.~Tofte and D.N.~Turner},
  title = 	{The {ML Kit}, {Version 1}},
  institution = {Department of Computer Science, University of Copenhagen},
  year = 	1993,
  number = 	{93/14},
  note = 	{(112 pages)},
  url =         {http://www.itu.dk/research/mlkit},
  postscript =  {mlkit1.ps.gz}
}

@Article{BirkedalL:btasml,
  author = 	 {L.~Birkedal and M.~Welinder},
  title = 	 {Binding-Time Analysis for {Standard} {ML}},
  journal = 	 {Lisp and Symbolic Computation},
  year = 	 1995,
  volume =	 8,
  number =	 3,
  month =	 {September},
  pages =	 {191--208},
  postscript =   {btasml.ps.gz}
}

@InProceedings{BirkedalL:btasml:pepm,
  author = 	 "L.~Birkedal and M.~Welinder",
  title = 	 "Binding-Time Analysis for {Standard} {ML}",
  pages = 	 "61--71",
  booktitle =    "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",
  year = 	 1994,
  note = 	 {Superseded by~\cite{BirkedalL:btasml}},
  postscript =   {btasml:pepm.ps.gz}
}

@InProceedings{BirkedalL:hanpgg,
  author = 	 "L.~Birkedal and M.~Welinder",
  title = 	 "Handwriting Program Generator Generators",
  editor = 	 "Manuel Hermenegildo and Jaan Penjam",
  pages = 	 "198--214",
  booktitle =    "Programming Language Implementation and Logic
		  Programming. 6th International Symposium, PLILP '94",
  year = 	 1994,
  volume =       844,
  series =       "Lecture Notes in Computer Science",
  publisher = "Springer",
  address = 	 "Madrid, Spain",
  month = 	 sep,
  postscript =   {hanpgg.ps.gz}
}

@TechReport{BirkedalL:paresm,
  author = 	"L.~Birkedal and M.~Welinder",
  title = 	"Partial Evaluation of {Standard} {ML}",
  institution = "DIKU, Department of Computer Science, 
                 University of Copenhagen",
  year = 	1993,
  number = 	"93/22",
  month = 	oct,
  note =	"Master's Thesis. (173 pages)",
  postscript =  {paresm.ps.gz}
}

@Unpublished{BirkedalL:higofp,
  author = 	"L.~Birkedal",
  title = 	"Higher-order Functors and Principal Signatures in
		 {Standard} {ML}",
  note = 	"TOPPS Report D--184 (117 pages)",
  address =      "Department of Computer Science, University of Copenhagen",
  year = 	"1993",
  month = 	sep,
  postscript =  {higofp.ps.gz}
}

@Unpublished{BirkedalL:towsfb,
  author = 	"L.~Birkedal and N.J.~Rehof",
  title = 	"Towards a Semantic Foundation for Binding Time Analysis",
  note = 	"DIKU Student Project",
  year = 	1993,
  month = 	apr
}