| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Lars Birkedal, Kristian Støvring, Jacob Thamsborg |
A relational realizability model for higher-order stateful ADTs.  |
J. Log. Algebr. Program.  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, Peter Sestoft |
Formalized Verification of Snapshotable Trees: Separation and Sharing. |
VSTTE |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal (eds.) |
Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings |
FOSSACS |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Jonas Braband Jensen, Lars Birkedal |
Fictional Separation Logic. |
ESOP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Jonas Braband Jensen, Lars Birkedal, Peter Sestoft |
Modular Verification of Linked Lists with Views via Separation Logic. |
Journal of Object Technology |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexandre Buisse, Lars Birkedal, Kristian Støvring |
Step-Indexed Kripke Model of Separation Logic for Storable Locks. |
Electr. Notes Theor. Comput. Sci. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang |
Nested Hoare Triples and Frame Rules for Higher-order Store |
Logical Methods in Computer Science |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Derek Dreyer, Amal Ahmed, Lars Birkedal |
Logical Step-Indexed Logical Relations |
Logical Methods in Computer Science |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski |
Partiality, State and Dependent Types. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob Thamsborg, Hongseok Yang |
Step-indexed kripke models over recursive worlds. |
POPL |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal |
Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacob Thamsborg, Lars Birkedal |
A kripke logical relation for effect-based program transformations. |
ICFP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, Kristian Støvring |
First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees. |
LICS |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jan Schwinghammer, Lars Birkedal |
Step-Indexed Relational Reasoning for Countable Nondeterminism. |
CSL |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jan Schwinghammer, Lars Birkedal, Kristian Støvring |
A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces. |
FOSSACS |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Kristian Støvring, Jacob Thamsborg |
The category-theoretic solution of recursive metric-space equations. |
Theor. Comput. Sci. |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Kristian Støvring, Jacob Thamsborg |
Realisability semantics of parametric polymorphism, general references and recursive types. |
Mathematical Structures in Computer Science |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Derek Dreyer, Georg Neis, Andreas Rossberg, Lars Birkedal |
A relational modal logic for higher-order stateful ADTs. |
POPL |
2010 |
DBLP DOI BibTeX RDF |
local state, plotkin-abadi logic, modal logic, abstract data types, separation logic, step-indexed logical relations |
| 1 | Derek Dreyer, Georg Neis, Lars Birkedal |
The impact of higher-order state and control effects on local relational reasoning. |
ICFP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Neel Krishnaswami, Lars Birkedal, Jonathan Aldrich |
Verifying event-driven programs using ramified frame properties. |
TLDI |
2010 |
DBLP DOI BibTeX RDF |
frame rule, ramification problem, subject-observer, dataflow, separation logic, functional reactive programming |
| 1 | Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson |
Verifying Generics and Delegates. |
ECOOP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, Bernhard Reus |
A Semantic Foundation for Hidden State. |
FOSSACS |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal, Kasper Svendsen, Alexandre Buisse |
Design patterns in separation logic. |
TLDI |
2009 |
DBLP DOI BibTeX RDF |
design patterns, separation logic |
| 1 | Lars Birkedal, Kristian Støvring, Jacob Thamsborg |
Relational parametricity for references and recursive types. |
TLDI |
2009 |
DBLP DOI BibTeX RDF |
general references, impredicative polymorphism, denotational semantics, recursive types, relational parametricity, possible world semantics |
| 1 | Derek Dreyer, Amal Ahmed, Lars Birkedal |
Logical Step-Indexed Logical Relations. |
LICS |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang |
Nested Hoare Triples and Frame Rules for Higher-Order Store. |
CSL |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Kristian Støvring, Jacob Thamsborg |
Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types. |
FOSSACS |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Hongseok Yang |
Relational Parametricity and Separation Logic. |
Logical Methods in Computer Science |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Carsten Varming, Lars Birkedal |
Higher-Order Separation Logic in Isabelle/HOLCF. |
Electr. Notes Theor. Comput. Sci. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Rasmus Ejlers Møgelberg, Lars Birkedal, Giuseppe Rosolini |
Synthetic domain theory and models of linear Abadi & Plotkin logic. |
Ann. Pure Appl. Logic |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Noah Torp-Smith, Lars Birkedal, John C. Reynolds |
Local reasoning about a copying garbage collector. |
ACM Trans. Program. Lang. Syst. |
2008 |
DBLP DOI BibTeX RDF |
copying garbage collector, Separation logic, local reasoning |
| 1 | Lars Birkedal, Hongseok Yang |
Relational Parametricity and Separation Logic |
CoRR |
2008 |
DBLP BibTeX RDF |
|
| 1 | Aleksandar Nanevski, J. Gregory Morrisett, Lars Birkedal |
Hoare type theory, polymorphism and separation. |
J. Funct. Program. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Søren Debois, Thomas T. Hildebrandt |
On the Construction of Sorted Reactive Systems. |
CONCUR |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Hongseok Yang |
A Simple Model of Separation Logic for Higher-Order Store. |
ICALP |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal |
Ynot: dependent types for imperative programs. |
ICFP |
2008 |
DBLP DOI BibTeX RDF |
type theory, monads, Hoare logic, separation logic |
| 1 | Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett |
A Realizability Model for Impredicative Hoare Type Theory. |
ESOP |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen |
Domain-theoretical models of parametric polymorphism. |
Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal |
Book Reviews. |
Studia Logica |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Troels Christoffer Damgaard, Arne J. Glenstrup, Robin Milner |
Matching of Bigraphs. |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Bodil Biering, Lars Birkedal, Noah Torp-Smith |
BI-hyperdoctrines, higher-order separation logic, and abstraction. |
ACM Trans. Program. Lang. Syst. |
2007 |
DBLP DOI BibTeX RDF |
hyperdoctrines, abstraction, Separation logic |
| 1 | Lars Birkedal, Hongseok Yang |
Relational Parametricity and Separation Logic. |
FoSSaCS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal |
Abstract Predicates and Mutable ADTs in Hoare Type Theory. |
ESOP |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Noah Torp-Smith, Hongseok Yang |
Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages. |
Logical Methods in Computer Science |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen |
Linear Abadi and Plotkin Logic. |
Logical Methods in Computer Science |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Rasmus Ejlers Møgelberg, Lars Birkedal, Giuseppe Rosolini |
Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic. |
Electr. Notes Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen |
Parametric Domain-theoretic Models of Polymorphic Intuitionistic / Linear Lambda Calculus. |
Electr. Notes Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Noah Torp-Smith, Hongseok Yang |
Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages |
CoRR |
2006 |
DBLP BibTeX RDF |
|
| 1 | Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen |
Linear Abadi and Plotkin Logic |
CoRR |
2006 |
DBLP BibTeX RDF |
|
| 1 | Troels Christoffer Damgaard, Lars Birkedal |
Axiomatizing Binding Bigraphs. |
Nord. J. Comput. |
2006 |
DBLP BibTeX RDF |
|
| 1 | Lars Birkedal, Søren Debois, Thomas T. Hildebrandt |
Sortings for Reactive Systems. |
CONCUR |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Aleksandar Nanevski, Greg Morrisett, Lars Birkedal |
Polymorphism and separation in hoare type theory. |
ICFP |
2006 |
DBLP DOI BibTeX RDF |
type theory, hoare logic, separation logic |
| 1 | Nina Bohr, Lars Birkedal |
Relational Reasoning for Recursive Types and References. |
APLAS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Søren Debois, Ebbe Elsborg, Thomas T. Hildebrandt, Henning Niss |
Bigraphical Models of Context-Aware Systems. |
FoSSaCS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Rasmus Ejlers Møgelberg |
Categorical models for Abadi and Plotkin's logic for parametricity. |
Mathematical Structures in Computer Science |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Noah Torp-Smith, Hongseok Yang |
Semantics of Separation-Logic Typing and Higher-Order Frame Rules. |
LICS |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Bodil Biering, Lars Birkedal, Noah Torp-Smith |
BI Hyperdoctrines and Higher-Order Separation Logic. |
ESOP |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrej Bauer, Lars Birkedal, Dana S. Scott |
Equilogical spaces. |
Theor. Comput. Sci. |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Martín Hötzel Escardó, Achim Jung, Giuseppe Rosolini |
Preface: Recent Developments in Domain Theory: A collection of papers in honour of Dana S. Scott. |
Theor. Comput. Sci. |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg |
A Retrospective on Region-Based Memory Management. |
Higher-Order and Symbolic Computation |
2004 |
DBLP DOI BibTeX RDF |
dynamic storage management, regions, Standard ML |
| 1 | Lars Birkedal, Noah Torp-Smith, John C. Reynolds |
Local reasoning about a copying garbage collector. |
POPL |
2004 |
DBLP DOI BibTeX RDF |
copying garbage collector, separation logic, local reasoning |
| 1 | Steven Awodey, Lars Birkedal, Dana S. Scott |
Local Realizability Toposes and a Modal Logic for Computability. |
Mathematical Structures in Computer Science |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal |
A general notion of realizability. |
Bulletin of Symbolic Logic |
2002 |
DBLP BibTeX RDF |
|
| 1 | Lars Birkedal, Jaap van Oosten |
Relative and modified relative realizability. |
Ann. Pure Appl. Logic |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Mads Tofte |
A constraint-based region inference algorithm. |
Theor. Comput. Sci. |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal |
On propositions-as-types in realizability models. |
Electr. Notes Theor. Comput. Sci. |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal |
Developing Theories of Types and Computability via Realizability. |
Electr. Notes Theor. Comput. Sci. |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Mads Tofte, Lars Birkedal |
Unification and polymorphism in region inference. |
Proof, Language, and Interaction |
2000 |
DBLP BibTeX RDF |
|
| 1 | Lars Birkedal |
A General Notion of Realizability. |
LICS |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrej Bauer, Lars Birkedal |
Continuous Functionals of Dependent Types and Equilogical Spaces. |
CSL |
2000 |
DBLP DOI BibTeX RDF |
dependent type theory, equilogical spaces, domain theory, continuous functionals |
| 1 | Lars Birkedal, Robert Harper |
Relational Interpretations of Recursive Types in an Operational Setting. |
Inf. Comput. |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Jaap van Oosten, Giuseppe Rosolini, Dana S. Scott |
Preface. |
Electr. Notes Theor. Comput. Sci. |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Steven Awodey, Lars Birkedal, Dana S. Scott |
Local Realizability Toposes and a Modal Logic for Computability. |
Electr. Notes Theor. Comput. Sci. |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal |
Bibliography on Realizability. |
Electr. Notes Theor. Comput. Sci. |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Mads Tofte, Lars Birkedal |
A Region Inference Algorithm. |
ACM Trans. Program. Lang. Syst. |
1998 |
DBLP DOI BibTeX RDF |
regions, standard ML |
| 1 | Lars Birkedal, Aurelio Carboni, Giuseppe Rosolini, Dana S. Scott |
Type Theory via Exact Categories. |
LICS |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Robert Harper |
Relational Interpretations of Recursive Types in an operational Setting (Summary). |
TACS |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Mads Tofte, Magnus Vejlstrup |
From Region Inference to von Neumann Machines via Region Representation Inference. |
POPL |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Birkedal, Morten Welinder |
Binding-Time Analysis for Standard ML. |
Lisp and Symbolic Computation |
1995 |
DBLP BibTeX RDF |
|
| 1 | Lars Birkedal, Morten Welinder |
Binding-Time Analysis for Standard ML. |
PEPM |
1994 |
DBLP BibTeX RDF |
|
| 1 | Lars Birkedal, Morten Welinder |
Hand-Writing Program Generator Generators. |
PLILP |
1994 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")