%%% ====================================================================
%%% BibTeX-file{
%%% author = "Lars Birkedal",
%%% date = "2020",
%%% filename = "BirkedalL.bib",
%%% url = "http://users-cs.au.dk/birke/papers/BirkedalL.bib",
%%% www-home = "http://users-cs.au.dk/birke/",
%%% email = "birkedal at cs.au.dk",
%%% dates = {1990--},
%%% keywords = "",
%%% supported = "yes",
%%% supported-by = "Lars Birkedal",
%%% abstract = "Bibliography for Lars Birkedal"
%%% }
%%% ====================================================================
@InProceedings{BirkedalL:caps-mmio-conf,
author = {T. Van Strydonck and A.L. Georges and A. Gueneau and A. Trieu and A. Timany and F. Piessens and L. Birkedal and D. Devriese},
title = {Proving Full-System Security Properties under Multiple Attacker Models on Capability Machines},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of CSF},
year = {2022},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTpages = {},
OPTmonth = {},
OPTaddress = {},
OPTorganization = {},
OPTpublisher = {},
note = {Accepted for publication},
annote = {caps-mmio-conf.pdf}
}
@InProceedings{BirkedalL:free-theorems-sep-logic,
author = {L. Birkedal and T. Dinsdale-Young and A. Gueneau and G. Jaber and K. Svendsen and N. Tzevelekos},
title = {Theorems for Free from Separation Logic Specifications},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ICFP},
year = {2021},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTpages = {},
OPTmonth = {},
OPTaddress = {},
OPTorganization = {},
OPTpublisher = {},
OPTnote = {},
annote = {free-theorems-sep-logic.pdf}
}
@InProceedings{BirkedalL:coexp-conf,
author = {Z. Qian and A.G. Kavvos and L. Birkedal},
title = {Client-Server Sessions in Linear Logic},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ICFP},
year = {2021},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTpages = {},
OPTmonth = {},
OPTaddress = {},
OPTorganization = {},
OPTpublisher = {},
OPTnote = {},
annote = {coexp-conf.pdf}
}
@Article{BirkedalL:modalities-and-parametric-adjoints,
author = {D. Gratzer and E. Cavallo and G.A. Kavvos and A.. Guatto and L. Birkedal.},
title = {Modalities and Parametric Adjoints},
journal = {},
year = {2021},
OPTkey = {},
OPTvolume = {},
OPTnumber = {},
OPTpages = {},
OPTmonth = {},
note = {Submitted for publication},
OPTannote = {}
}
@Article{BirkedalL:mtt-journal,
author = {D. Gratzer, G.A. Kavvos, A. Nuyts, and L. Birkedal},
title = {Multimodal Dependent Type Theory},
journal = {},
year = {2020},
OPTkey = {},
OPTvolume = {},
OPTnumber = {},
OPTpages = {},
OPTmonth = {},
note = {Submitted for publication},
OPTannote = {}
}
@Article{BirkedalL:stk-tokens-journal,
author = {L. Skorstengaard and D. Devreise and L. Birkedal},
title = {{StkTokens}: Enforcing Well-Bracketed Control Flow and Stack Encapsulation using Linear Capabilities},
journal = {Journal of Functional Programming},
year = 2021,
volume = 31,
pdf = {stk-tokens-journal.pdf}
}
@Article{BirkedalL:reloc-journal,
author = {D. Frumin and R. Krebbers and L. Birkedal},
title = {ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity},
journal = {},
year = {2020},
OPTkey = {},
OPTvolume = {},
OPTnumber = {},
OPTpages = {},
OPTmonth = {},
note = {Submitted for publication},
OPTannote = {}
}
@InProceedings{BirkedalL:iris-caps-jfla,
author = {A.L. Georges and A. Gueneau and T. van Strydonck and A. Timany and A. Trieu and D. Devriese and L. Birkedal},
title = {Cap' ou pas cap' ? Preuve de programmes pour une machine {\'a} capacit{\'e}s en pr{\'e}sence de code inconnu},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of JFLA'21: Journees Francophones des Langages Applicatifs},
OPTpages = {},
year = 2021,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
pdf = {iris-caps-jfla.pdf}
}
@InProceedings{BirkedalL:ms-queue-conf,
author = {S.F. Vindum and L. Birkedal},
title = {Contextual Refinement of the Michael-Scott Queue (Proof Pearl)},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of CPP},
OPTpages = {},
year = 2021,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
pdf = {2021-ms-queue.pdf}
}
@InProceedings{BirkedalL:monotone-conf,
author = {A. Timany and L. Birkedal},
title = {Reasoning About Monotonicity in Separation Logic},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of CPP},
OPTpages = {},
year = 2021,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
pdf = {2021-monotone.pdf}
}
@InProceedings{BirkedalL:ccddb-conf,
author = {L. Gondelman and S.O. Gregersen and A. Nieto and A. Timany and L. Birkedal},
title = {Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic.},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of POPL},
OPTpages = {},
year = 2021,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
pdf = {2021-ccddb.pdf}
}
@InProceedings{BirkedalL:iris-caps-conf,
author = {A.L. Georges and A. Gueneau and T. van Strydonck and A. Timany and A. Trieu and S. Huyghebaert and D. Devriese and L. Birkedal},
title = {Efficient and Provable Local Capability Revocation using Uninitialized Capabilities},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of POPL},
OPTpages = {},
year = 2021,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
pdf = {2021-iris-caps.pdf}
}
@InProceedings{BirkedalL:tiniris-conf,
author = {S.O. Gregersen and J. Bay and A. Timany and L. Birkedal}
title = {Mechanized Logical Relations for Termination-Insensitive Noninterference.},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of POPL},
OPTpages = {},
year = 2021,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
pdf = {2021-tiniris.pdf}
}
@InProceedings{BirkedalL:mtt-conf,
author = {D. Gratzer and G.A. Kavvos and A. Nuyts and L. Birkedal},
title = {Multimodal Dependent Type Theory},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of LICS},
OPTpages = {},
year = 2020,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
pdf = {mtt-conf.pdf}
}
@InProceedings{BirkedalL:gdot-conf,
author = {P.G. Giarrusso and L. Stefanesco and A. Timany and L. Birkedal and R. Krebbers},
title = {Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ICFP},
year = {2020},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTpages = {},
OPTmonth = {},
OPTaddress = {},
OPTorganization = {},
OPTpublisher = {},
OPTnote = {},
OPTannote = {},
pdf = {gdot-icfp20-1.0.pdf}
}
@InProceedings{BirkedalL:seloc-conf,
author = {D. Frumin and R. Krebbers and L. Birkedal},
title = {Compositional Non-Interference for Fine-Grained Concurrent Programs}
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of Security and Privacy},
OPTpages = {},
year = 2021,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
pdf = {seloc-conf.pdf}
}
@InProceedings{BirkedalL:aneris-conf,
author = {M. Krogh-Jespersen and A. Timany and M.E. Ohlenbusch and S.O. Gregersen, and L. Birkedal}
title = {Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ESOP 2020},
OPTpages = {},
year = 2019,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
pdf = {aneris-conf.pdf}
}
@InProceedings{BirkedalL:iris-capabilities-prisc-conf,
author = {A.L. Georges and A. Trieue and L. Birkedal},
title = {Mechanized Reasoning about a Capability Machine},
OPTcrossref = {},
OPTkey = {},
OPTbooktitle = {}
OPTpages = {},
year = 2020,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
pdf = {iris-capabilities-prisc-conf.pdf},
note = {Extended abstract for talk at the PRISC 2020 workshop}
}
@InProceedings{BirkedalL:implementing-modal-dependent-type-theory-conf,
author = {D. Gratzer and J. Sterling and L. Birkedal},
title = {Implementing a Modal Dependent Type Theory},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ICFP 2019},
OPTpages = {},
year = 2019,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
pdf = {implementing-modal-dependent-type-theory-conf.pdf},
note = {Distinguished Paper Award}
}
@InProceedings{BirkedalL:iris-logrel-cc-conf,
author = {A. Timany and L. Birkedal},
title = {Mechanized Relational Verification of Concurrent Programs with Continuations},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ICFP 2019},
OPTpages = {},
year = 2019,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
pdf = {iris-logrel-cc-conf.pdf}
}
@Article{BirkedalL:dradjoint,
author = {L. Birkedal and R. Clouston and B. Mannaa and R.E. M{\o}gelberg and A.M. Pitts and B. Spitters},
title = {Modal Dependent Type Theory and Dependent Right Adjoints},
journal = {Mathematical Structures in Computer Science},
year = {2019},
OPTkey = {},
OPTvolume = {},
OPTnumber = {},
pages = {1--21},
OPTmonth = {},
OPTannote = {},
pdf = {dradjoint.pdf}
}
@InProceedings{BirkedalL:iron-conf,
author = {A. Bizjak and D. Gratzer and R. Krebbers and L. Birkedal},
title = {{Iron:} Managing Obligations in
Higher-Order Concurrent Separation Logic},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of POPL 2019},
OPTpages = {},
year = 2019,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
pdf = {iron-conf.pdf}
}
@InProceedings{BirkedalL:stk-tokens-conf,
author = {L. Skorstengaard and D. Devriese and L. Birkedal},
title = {{StkTokens:} Enforcing Well-Bracketed Control Flow and
Stack Encapsulation Using Linear Capabilities},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of POPL 2019},
OPTpages = {},
year = 2019,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
pdf = {stk-tokens-conf.pdf}
}
@Article{BirkedalL:gdtt-cubical-journal,
author = {L. Birkedal and A. Bizjak and R. Clouston and H.B. Grathwohl and B. Spitters and A. Vezzosi},
title = {Guarded Cubical Type Theory},
OPTcrossref = {},
OPTkey = {},
journal = {Journal of Automated Reasoning, special issue of HoTT/UF},
pages = {211--263},
year = 2018,
OPTeditor = {},
volume = {63},
number = {2},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {gctt-journal.pdf}
doi = {https://link.springer.com/article/10.1007/s10817-018-9471-7}
}
@Article{BirkedalL:local-capabilities-journal,
author = {L. Skorstengaard and D. Devriese and L. Birkedal},
title = {Reasoning about a Capability Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management},
year = 2018,
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)}
number = {5},
pdf = {local-capabilities-journal.pdf}
}
@InProceedings{BirkedalL:reloc-conf,
author = {D. Frumin and R. Krebbers and L. Birkedal},
title = {{ReLoC:} A Mechanised Relational Logic for Fine-Grained Concurrency},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of LICS 2018},
OPTpages = {},
year = 2018,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
pdf = {reloc-conf.pdf}
}
@Article{BirkedalL:iris-journal,
author = {R. Jung and R. Krebbers and J-H. Jourdan and A. Bizjak and L. Birkedal and D. Dreyer},
title = {Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic},
journal = {Journal of Functional Programming},
year = {2018},
OPTkey = {},
volume = {28},
OPTnumber = {},
OPTpages = {},
OPTmonth = {},
OPTannote = {},
pdf = {iris-journal.pdf}
}
@Article{BirkedalL:guarded-equilogical,
author = {A. Bizjak and L. Birkedal},
title = {A Model of Guarded Recursion via Generalised Equilogical Spaces},
journal = {Theoretical Computer Science},
year = {2018},
OPTkey = {},
volume = {772},
OPTnumber = {},
pages = {1--18},
OPTmonth = {},
OPTannote = {},
pdf = {guarded-equilogical-journal.pdf}
}
@InProceedings{BirkedalL:noninterference-concurrent-conf,
author = {A. Karbyshev and K. Svendsen and A. Askarov and L. Birkedal},
title = {Compositional Non-Interference for Concurrent Programs via Separation and Framing},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of POST 2018},
OPTpages = {},
year = 2018,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {noninterference-concurrent-conf.pdf}
}
@InProceedings{BirkedalL:guarded-hol-probability,
author = {A. Aguirre and G. Barthe and L. Birkedal and A. Bizjak and M. Gaboardi and D. Garg},
title = {Relational Reasoning for {Markov} Chains in a Probabilistic Guarded Lambda Calculus},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ESOP 2018},
OPTpages = {},
year = 2018,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {guarded-hol-probability-conf}
}
@InProceedings{BirkedalL:local-capabilities-conf,
author = {L. Skorstengaard and D. Devriese and L. Birkedal},
title = {Reasoning about a Capability Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management (without {OS} Support)},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ESOP 2018},
OPTpages = {},
year = 2018,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {local-capabilities-conf.pdf}
}
@TechReport{BirkedalL:local-capabilities-conf-tr,
author = {L. Skorstengaard and D. Devriese and L. Birkedal},
title = {Reasoning about a Capability Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management (without {OS} Support). {Technical Appendix} including Proofs and Details},
institution = {Aarhus University},
OPTpages = {},
year = 2018,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {local-capabilities-conf-tr.pdf}
}
@InProceedings{BirkedalL:runST-conf,
author = {A. Timany and L. Stefanesco and M. Krogh-Jespersen and L. Birkedal},
title = {A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of \texttt{runST}},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of POPL},
OPTpages = {},
year = 2018,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {runST-conf.pdf}
}
@InProceedings{BirkedalL:box-modality-conf,
author = {A. Bizjak and L. Birkedal},
title = {On Models of Higher-Order Separation Logic},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of MFPS2017},
OPTpages = {},
year = 2017,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {box-modality-conf.pdf}
}
@InProceedings{BirkedalL:iris3-conf,
author = {R. Krebbers and R. Jung and A. Bizjak and J.-H. Jourdan and D. Dreyer and L. Birkedal},
title = {The Essence of Higher-Order Concurrent Separation Logic},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ESOP 2017},
OPTpages = {},
year = 2017,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {iris3-conf.pdf}
}
@InProceedings{BirkedalL:caper-conf,
author = {T. Dinsdale-Young and P. Pinto and K.J. Andersen and L. Birkedal},
title = {Caper: Automatic Verification for Fine-Grained Concurrency},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ESOP 2017},
OPTpages = {},
year = 2017,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {caper-conf.pdf}
}
@InProceedings{BirkedalL:iris-effects-conf,
author = {M. Krogh-Jespersen and K. Svendsen and L. Birkedal},
title = {A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of POPL 2017},
OPTpages = {},
year = 2017,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {iris-effects-conf.pdf}
}
@InProceedings{BirkedalL:ipm-conf,
author = {R. Krebbers and A. Timany and L. Birkedal},
title = {Interactive Proofs in Higher-Order Concurrent Separation Logic},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of POPL 2017},
OPTpages = {},
year = 2017,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {ipm-conf.pdf}
}
@InProceedings{BirkedalL:gdtt-cubical-conf,
author = {L. Birkedal and A. Bizjak and R. Clouston and H.B. Grathwohl and B. Spitters and A. Vezzosi},
title = {Guarded Cubical Type Theory: Path Equality for Guarded Recursion},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of CSL 2016 (accepted for publication)},
OPTpages = {},
year = 2016,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {gdtt-cubical-conf.pdf}
}
@InProceedings{BirkedalL:iris-2.0-confs,
author = {R. Jung and R. Krebbers and L. Birkedal and D. Dreyer},
title = {Higher-Order Ghost State},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ICFP 2016},
OPTpages = {},
year = 2016,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {iris-2.0-conf.pdf}
}
@Article{BirkedalL:guarded-lambda-journal,
author = {R. Clouston and A. Bizjak and H. Bugge Grathwohl and L. Birkedal},
title = {The Guarded Lambda Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types},
journal = {Logical Methods in Computer Science},
OPTcrossref = {},
OPTkey = {},
OPTpages = {},
year = 2016,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
note = {Accepted for publication (journal version of FOSSACS 2015 paper)},
pdf = {guarded-lambda-journal.pdf}
}
@Article{BirkedalL:effect-journal,
author = {L. Birkedal and G. Jaber and F. Sieczkowski and J. Thamsborg},
title = {A {Kripke} Logical Relation for Effect-Based Program Transformations},
journal = {Information and Computation},
year = {2016},
OPTkey = {},
OPTvolume = {},
OPTnumber = {},
OPTpages = {},
OPTmonth = {},
note = {Accepted for publication},
OPTannote = {},
pdf = {effects-journal.pdf}
}
@InProceedings{BirkedalL:gctt-typess,
author = {L. Birkedal and A. Bizjak and R. Clouston and H.B. Gratwohl and B. Spitters and A. Vezzosi},
title = {Guarded Cubical Type Theory},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of Types 2016},
OPTpages = {},
year = 2016,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {gctt-types.pdf}
}
@InProceedings{BirkedalL:biglater,
author = {K. Svendsen and F. Sieczkowski and L. Birkedal},
title = {Transfinite Step-indexing: Decoupling Concrete and Logical Steps},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ESOP 2016},
OPTpages = {},
year = 2016,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {biglater-conf.pdf}
}
@InProceedings{BirkedalL:gdtt-conf,
author = {A. Bizjak and H.B. Grathwohl and R. Clouston and R.E. M{\o}gelberg and L. Birkedal},
title = {Guarded Dependent Type Theory with Coinductive Types},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of FOSSACS 2016},
OPTpages = {},
year = 2016,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {gdtt-conf.pdf}
}
@InProceedings{BirkedalL:object-capabilities-conf,
author = {D. Devriese and F. Piessens and L. Birkedal},
title = {Reasoning about Object Capabilities with Logical Relations and Effect Parametricity},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of EuroS&P 2016},
OPTpages = {},
year = 2016,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {object-capabilities-conf.pdf}
}
@TechReport{{BirkedalL:object-capabilities-conf,
author = {D. Devriese and F. Piessens and L. Birkedal},
title = {Reasoning about Object Capabilities with Logical Relations and Effect Parametricity (Technical Report including Proofs and Details)},
institution = {KU Leuven},
year = {2016},
OPTkey = {},
OPTtype = {},
number = {CW~690},
OPTaddress = {},
month = jan,
OPTnote = {},
OPTannote = {},
pdf = {object-capabilities-tr.pdf}
}
@Article{BirkedalL:futureproof,
author = {M. Dodds and S. Jagannathan and M.J. Parkinson and K. Svendsen and L. Birkedal},
title = {Verifying Custom Synchronisation Constructs Using Higher-Order Separation Logic},
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
year = {2016},
volume = {38},
number = {2:4},
OPTpages = {},
OPTmonth = {},
OPTannote = {},
pdf = {futureproof.pdf}
}
@InProceedings{BirkedalL:pcf-in-sf,
author = {M. Paviotti and R.E. M{\o}gelberg and L. Birkedal},
title = {A Model of {PCF} in Guarded Type Theory},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proocedings of MFPS},
OPTpages = {},
year = 2015,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {pcf-in-s.pdf}
}
@InProceedings{BirkedalL:modures-coq-conf,
author = {F. Sieczkowski and A. Bizjak and L. Birkedal},
title = {{ModuRes}: a {Coq} Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming Languages},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ITP},
OPTpages = {},
year = 2015,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTnote = {},
OPTannote = {},
pdf = {modures-coq-conf.pdf}
}
@InProceedings{BirkedalL:step-probability--conf,
author = {A. Bizjak and L. Birkedal},
title = {Step-Indexed Logical Relations for Probability},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of FOSSACS},
OPTpages = {},
year = 2015,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {step-probability-conf.pdf}
}
@InProceedings{BirkedalL:guarded-lambda-conf,
author = {R. Clouston and A. Bizjak and H. Bugge Grathwohl and L. Birkedal},
title = {Programming and Reasoning with Guarded Recursion for Coinductive Types},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of FOSSACS},
OPTpages = {},
year = 2015,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {guarded-lambda-conf.pdf}
}
@InProceedings{BirkedalL:icap-tso-conf,
author = {F. Sieczkowski and K. Svendsen and L. Birkedal and J. Pichon-Pharapod},
title = {A Separation Logic for Fictional Sequential Consistency},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ESOP},
OPTpages = {},
year = 2015,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {icap-tso-conf.pdf}
}
@InProceedings{BirkedalL:iris-conf,
author = {R. Jung and D. Swasey and F. Sieczkowski and K. Svendsen and A. Turon and L. Birkedal and D. Dreyer},
title = {Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of POPL},
OPTpages = {},
year = 2015,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {iris-conf.pdf}
}
@InProceedings{BirkedalL:internal-nondet-conf,
author = {A. Bizjak and L. Birkedal and M. Miculan},
title = {A Model of Countable Nondeterminism in Guarded Type Theory},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of TLCA},
OPTpages = {},
year = 2014,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {internal-nondet-conf.pdf}
}
@InProceedings{BirkedalL:icap-conf,
author = {K. Svendsen and L. Birkedal},
title = {Impredicative {C}oncurrent {A}bstract {P}redicates},
booktitle = {Proceedings of ESOP},
year = 2014,
pdf = {icap-conf.pdf}
}
@Article{Birkedal:step-nondet-journal,
author = {L. Birkedal and A. Bizjak and J. Schwinghammer},
title = {Step-Indexed Relational Reasoning for Countable Nondeterminism},
journal = {Logical Methods in Computer Science},
year = {2013},
volume = {9},
number = {4},
pages = {1--23},
month = oct,
OPTannote = {10.2168/LMCS-9(4:4)2013},
note = {lmcs online version},
pdf = {step-nondet-journal.pdf}
}
@InProceedings{BirkedalL:caresl-conf,
author = {A. Turon and D. Dreyer and L. Birkedal},
title = {Unifying Refinement and Hoare-Style Reasoning in a Logic for Higher-Order Concurrency},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ICFP},
OPTpages = {},
year = 2013,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTnote = {},
OPTannote = {},
pdf = {caresl.pdf}
}
@InProceedings{BirkedalL:sgdtuniverse-conf,
author = {L. Birkedal and R.E. M{\o}gelberg},
title = {Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of LICS},
OPTpages = {},
year = 2013,
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTnote = {},
OPTannote = {},
pdf = {sgdtuniverse-conf.pdf}
}
@InProceedings{BirkedalL:joins-conf,
author = {K. Svendsen and L. Birkedal and M. Parkinson},
title = {Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-order Library},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ECOOP},
OPTpages = {},
year = {2013},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTnote = {},
OPTannote = {},
pdf = {joins-conf.pdf}
}
@InProceedings{BirkedalL:hocap-conf,
author = {K. Svendsen and L. Birkedal and M. Parkinson},
title = {Modular Reasoning about Separation of Concurrent Data Structures},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of ESOP},
OPTpages = {},
year = {2013},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
OPTmonth = {},
OPTorganization = {},
OPTpublisher = {},
OPTnote = {},
OPTannote = {},
pdf = {hocap-conf.pdf}
}
@Misc{,
author = {Lars Birkedal and Ale\v{s} Bizjak},
title = {A note on the transitivity of step-indexed logical relations},
howpublished = {Manuscript},
month = nov,
year = {2012},
OPTnote = {},
OPTannote = {},
pdf = {step-transitivity.pdf}
}
@InProceedings{BirkedalL:relcon-conf,
author = {A. Turon and J. Thamsborg and A. Ahmed and L. Birkedal and D. Dreyer},
title = {Logical Relations for Fine-Grained Concurrency},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of POPL},
OPTpages = {},
year = {2013},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
month = jan,
OPTorganization = {},
OPTpublisher = {},
OPTnote = {},
OPTannote = {},
pdf = {relcon-conf.pdf}
}
@InProceedings{BirkedalL:views-conf,
author = {T. Dinsdale-Young and L. Birkedal and P. Gardner and M. Parkinson and H. Yang},
title = {Views: Compositional Reasoning for Concurrency},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of POPL},
OPTpages = {},
year = {2013},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
month = jan,
OPTorganization = {},
OPTpublisher = {},
OPTnote = {},
OPTannote = {},
pdf = {views.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 = {Logical Methods in Computer Science},
year = {2012},
OPTkey = {},
volume = {8},
number = {4},
OPTpages = {},
month = oct,
note = {lmcs online version},
OPTannote = {},
pdf = {sgdt-journal.pdf}
}
@article{BirkedalL:relational-lifting,
author = {J. Thamsborg and L. Birkedal and H. Yang},
title = {Two for the Price of One: Lifting Separation Logic Assertions},
journal = {Logical Methods in Computer Science},
year = 2012,
volume = 8,
number = 3,
month = sep,
note = {lmcs online version},
pdf = {relational-lifting.pdf}
}
@InProceedings{BirkedalL:relconc,
author = {L. Birkedal and F. Sieczkowski and J. Thamsborg},
title = {A Concurrent Logical Relation},
OPTcrossref = {},
OPTkey = {},
booktitle = {Proceedings of CSL},
OPTpages = {},
year = {2012},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
month = sep,
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {relconc.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 = {},
booktitle = {Proceedings of ITP},
OPTpages = {},
year = {2012},
OPTeditor = {},
OPTvolume = {},
OPTnumber = {},
OPTseries = {},
OPTaddress = {},
month = aug,
OPTorganization = {},
OPTpublisher = {},
OPTannote = {},
pdf = {charge-conf.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,
volume = 81,
number = 4,
pages = {491-521},
month = jan,
pdf = {relrmhoadt.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 = {{M}odelling, {C}ontrolling, and {R}easoning about {S}tate},
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{domultracoq.zip }},
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}
}
@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 = {lmcs online version},
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 = {lmcs online version}
}
@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 = {lmcs online version}
}
@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},
}
@Unpublished{BirekdalL:w-and-m-types-in-equ,
author = {A. Bauer and L. Birkedal},
title = {{W-Types} and {M-Types} in {E}quilogical {S}paces},
note = {Manuscript},
month = may,
year = {1999},
pdf = {w-m-types-in-equ.pdf}
}
@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
}