default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDLars Birkedal
Person information
- affiliation: Aarhus University, Denmark
SPARQL queries 
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[j77]Aïna Linn Georges
, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal:
Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code. J. ACM 71(1): 3:1-3:59 (2024)- [j76]Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal:
Almost-Sure Termination by Guarded Refinement. Proc. ACM Program. Lang. 8(ICFP): 203-233 (2024) - [j75]Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal:
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. Proc. ACM Program. Lang. 8(ICFP): 284-316 (2024) - [j74]Maxime Legoupil, June Rousseau, Aïna Linn Georges, Jean Pichon-Pharabod, Lars Birkedal:
Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly. Proc. ACM Program. Lang. 8(OOPSLA2): 304-332 (2024) - [j73]Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal:
Tachis: Higher-Order Separation Logic with Credits for Expected Costs. Proc. ACM Program. Lang. 8(OOPSLA2): 1189-1218 (2024) - [j72]Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, Lars Birkedal:
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement. Proc. ACM Program. Lang. 8(POPL): 241-272 (2024) - [j71]Dan Frumin, Amin Timany, Lars Birkedal:
Modular Denotational Semantics for Effects with Guarded Interaction Trees. Proc. ACM Program. Lang. 8(POPL): 332-361 (2024) - [j70]Amin Timany, Armaël Guéneau, Lars Birkedal:
The Logical Essence of Well-Bracketed Control Flow. Proc. ACM Program. Lang. 8(POPL): 575-603 (2024) - [j69]Angus Hammond, Zongyuan Liu, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod:
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic. Proc. ACM Program. Lang. 8(POPL): 604-637 (2024) - [j68]Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, Lars Birkedal:
The Essence of Generalized Algebraic Data Types. Proc. ACM Program. Lang. 8(POPL): 695-723 (2024) - [j67]Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal:
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. Proc. ACM Program. Lang. 8(POPL): 753-784 (2024) - [c101]Jonathan Sterling, Daniel Gratzer, Lars Birkedal:
Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. CSL 2024: 47:1-47:21 - [i31]Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal:
Almost-Sure Termination by Guarded Refinement. CoRR abs/2404.08494 (2024) - [i30]Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal:
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. CoRR abs/2404.14223 (2024) - [i29]Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal:
Tachis: Higher-Order Separation Logic with Credits for Expected Costs. CoRR abs/2405.20083 (2024) - [i28]Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal:
Approximate Relational Reasoning for Higher-Order Probabilistic Programs. CoRR abs/2407.14107 (2024) - [i27]Philipp Stassen, Rasmus Ejlers Møgelberg, Maaike Zwart, Alejandro Aguirre, Lars Birkedal:
Modelling Probabilistic FPC in Guarded Type Theory. CoRR abs/2408.04455 (2024) - 2023
- [j66]Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, Lars Birkedal:
Modular Verification of State-Based CRDTs in Separation Logic (Artifact). Dagstuhl Artifacts Ser. 9(2): 15:1-15:5 (2023) - [j65]Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, Lars Birkedal:
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols. Proc. ACM Program. Lang. 7(ICFP): 847-877 (2023) - [j64]Simon Friis Vindum, Lars Birkedal:
Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory. Proc. ACM Program. Lang. 7(OOPSLA2): 632-657 (2023) - [j63]Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer:
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. Proc. ACM Program. Lang. 7(OOPSLA2): 716-744 (2023) - [j62]Xiaojia Rao, Aïna Linn Georges, Maxime Legoupil, Conrad Watt, Jean Pichon-Pharabod, Philippa Gardner, Lars Birkedal:
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs. Proc. ACM Program. Lang. 7(PLDI): 1096-1120 (2023) - [j61]Zongyuan Liu, Sergei Stepanenko, Jean Pichon-Pharabod, Amin Timany, Aslan Askarov, Lars Birkedal:
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A. Proc. ACM Program. Lang. 7(PLDI): 1438-1462 (2023) - [j60]Alejandro Aguirre, Lars Birkedal:
Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice. Proc. ACM Program. Lang. 7(POPL): 33-60 (2023) - [c100]Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, Lars Birkedal:
Modular Verification of State-Based CRDTs in Separation Logic. ECOOP 2023: 22:1-22:27 - [c99]Frederik Lerbjerg Aagaard, Jonathan Sterling, Lars Birkedal:
A denotationally-based program logic for higher-order store. MFPS 2023 - [d17]Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal:
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic - Coq Artifact. Zenodo, 2023
- [d16]Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, Lars Birkedal:
The Essence of Generalized Algebraic Data Types. Version 1.0.0. Zenodo, 2023 [all versions] - [d15]Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, Lars Birkedal:
The Essence of Generalized Algebraic Data Types. Version 1.0.1. Zenodo, 2023 [all versions] - [d14]Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, Lars Birkedal:
The Essence of Generalized Algebraic Data Types. Version 1.1.0. Zenodo, 2023 [all versions] - [d13]Amin Timany, Armaël Guéneau, Lars Birkedal:
The Logical Essence of Well-Bracketed Control Flow (Artifact). Version 1. Zenodo, 2023 [all versions] - [d12]Amin Timany, Armaël Guéneau, Lars Birkedal:
The Logical Essence of Well-Bracketed Control Flow (Artifact). Version 2. Zenodo, 2023 [all versions] - [d11]Amin Timany, Armaël Guéneau, Lars Birkedal:
The Logical Essence of Well-Bracketed Control Flow (Artifact). Version 3. Zenodo, 2023 [all versions] - [d10]Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, Lars Birkedal:
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement - Coq Artifact. Zenodo, 2023 - [d9]Simon Friis Vindum, Lars Birkedal:
Artifact for the paper "Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory" in OOPSLA23. Version 1. Zenodo, 2023 [all versions] - [d8]Simon Friis Vindum, Lars Birkedal:
Artifact for the paper "Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory" in OOPSLA23. Version 2. Zenodo, 2023 [all versions] - [i26]Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal:
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. CoRR abs/2301.10061 (2023) - [i25]Dan Frumin, Amin Timany, Lars Birkedal:
Modular Denotational Semantics for Effects with Guarded Interaction Trees. CoRR abs/2307.08514 (2023) - [i24]Jonathan Sterling, Daniel Gratzer, Lars Birkedal:
Free theorems from univalent reference types. CoRR abs/2307.16608 (2023) - 2022
- [j59]Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer:
Later credits: resourceful reasoning for the later modality. Proc. ACM Program. Lang. 6(ICFP): 283-311 (2022) - [j58]Aïna Linn Georges, Alix Trieu, Lars Birkedal:
Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities. Proc. ACM Program. Lang. 6(OOPSLA1): 1-30 (2022) - [j57]Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, Lars Birkedal:
Modular verification of op-based CRDTs in separation logic. Proc. ACM Program. Lang. 6(OOPSLA2): 1788-1816 (2022) - [j56]Daniel Gratzer, Evan Cavallo, G. A. Kavvos, Adrien Guatto, Lars Birkedal:
Modalities and Parametric Adjoints. ACM Trans. Comput. Log. 23(3): 18:1-18:29 (2022) - [c98]Simon Friis Vindum, Dan Frumin, Lars Birkedal:
Mechanized verification of a fine-grained concurrent queue from meta's folly library. CPP 2022: 100-115 - [c97]Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese:
Proving full-system security properties under multiple attacker models on capability machines. CSF 2022: 80-95 - [c96]Daniel Gratzer, Lars Birkedal:
A Stratified Approach to Löb Induction. FSCD 2022: 23:1-23:22 - [c95]Philipp Stassen, Daniel Gratzer, Lars Birkedal:
{mitten}: A Flexible Multimodal Proof Assistant. TYPES 2022: 6:1-6:23 - [d7]Aïna Linn Georges, Alix Trieu, Lars Birkedal:
Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities (Artifact). Zenodo, 2022 - [d6]Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, Lars Birkedal:
Modular Verification of Op-Based CRDTs in Separation Logic (Proof Artifact). Version 1. Zenodo, 2022 [all versions] - [d5]Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, Lars Birkedal:
Modular Verification of Op-Based CRDTs in Separation Logic (Proof Artifact). Version 2. Zenodo, 2022 [all versions] - [i23]Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer, Lars Birkedal:
Unifying cubical and multimodal type theory. CoRR abs/2203.13000 (2022) - [i22]Jonathan Sterling, Daniel Gratzer, Lars Birkedal:
Denotational semantics of general store and polymorphism. CoRR abs/2210.02169 (2022) - [i21]Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal:
Controlling unfolding in type theory. CoRR abs/2210.05420 (2022) - 2021
- [j55]Lau Skorstengaard, Dominique Devriese, Lars Birkedal:
StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities. J. Funct. Program. 31: e9 (2021) - [j54]Dan Frumin, Robbert Krebbers, Lars Birkedal:
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. Log. Methods Comput. Sci. 17(3) (2021) - [j53]Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal:
Multimodal Dependent Type Theory. Log. Methods Comput. Sci. 17(3) (2021) - [j52]Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, Nikos Tzevelekos:
Theorems for free from separation logic specifications. Proc. ACM Program. Lang. 5(ICFP): 1-29 (2021) - [j51]Zesen Qian, G. A. Kavvos, Lars Birkedal:
Client-server sessions in linear logic. Proc. ACM Program. Lang. 5(ICFP): 1-31 (2021) - [j50]Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, Lars Birkedal:
Efficient and provable local capability revocation using uninitialized capabilities. Proc. ACM Program. Lang. 5(POPL): 1-30 (2021) - [j49]Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, Lars Birkedal:
Distributed causal memory: modular specification and verification in higher-order distributed separation logic. Proc. ACM Program. Lang. 5(POPL): 1-29 (2021) - [j48]Simon Oddershede Gregersen, Johan Bay, Amin Timany, Lars Birkedal:
Mechanized logical relations for termination-insensitive noninterference. Proc. ACM Program. Lang. 5(POPL): 1-29 (2021) - [c94]Simon Friis Vindum, Lars Birkedal:
Contextual refinement of the Michael-Scott queue (proof pearl). CPP 2021: 76-90 - [c93]Amin Timany, Lars Birkedal:
Reasoning about monotonicity in separation logic. CPP 2021: 91-104 - [c92]Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal:
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. PLDI 2021: 80-95 - [c91]Dan Frumin, Robbert Krebbers, Lars Birkedal:
Compositional Non-Interference for Fine-Grained Concurrent Programs. SP 2021: 1416-1433 - [d4]Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese:
Proving full-system security properties under multiple attacker models on capability machines: Coq mechanization. Zenodo, 2021 - [d3]Simon Friis Vindum, Dan Frumin, Lars Birkedal:
Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Library - Coq Artefact. Version 1.0.0. Zenodo, 2021 [all versions] - [d2]Simon Friis Vindum, Dan Frumin, Lars Birkedal:
Coq development for "Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Library". Version 1.0.0. Zenodo, 2021 [all versions] - [i20]Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Léon Gondelman, Abel Nieto, Lars Birkedal:
Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic. CoRR abs/2109.07863 (2021) - 2020
- [j47]Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters:
Modal dependent type theory and dependent right adjoints. Math. Struct. Comput. Sci. 30(2): 118-138 (2020) - [j46]Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, Robbert Krebbers:
Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris. Proc. ACM Program. Lang. 4(ICFP): 114:1-114:29 (2020) - [j45]Lau Skorstengaard, Dominique Devriese, Lars Birkedal:
Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management. ACM Trans. Program. Lang. Syst. 42(1): 5:1-5:53 (2020) - [c90]Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, Lars Birkedal:
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. ESOP 2020: 336-365 - [c89]Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal:
Multimodal Dependent Type Theory. LICS 2020: 492-506 - [d1]Simon Friis Vindum, Lars Birkedal:
Contextual Refinement of the Michael-Scott Queue - Coq Artifact. Zenodo, 2020 - [i19]Dan Frumin, Robbert Krebbers, Lars Birkedal:
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. CoRR abs/2006.13635 (2020) - [i18]Zesen Qian, G. A. Kavvos, Lars Birkedal:
Client-Server Sessions in Linear Logic. CoRR abs/2010.13926 (2020) - [i17]Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal:
Multimodal Dependent Type Theory. CoRR abs/2011.15021 (2020)
2010 – 2019
- 2019
- [j44]Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi:
Guarded Cubical Type Theory. J. Autom. Reason. 63(2): 211-253 (2019) - [j43]Amin Timany, Lars Birkedal:
Mechanized relational verification of concurrent programs with continuations. Proc. ACM Program. Lang. 3(ICFP): 105:1-105:28 (2019) - [j42]Daniel Gratzer, Jonathan Sterling, Lars Birkedal:
Implementing a modal dependent type theory. Proc. ACM Program. Lang. 3(ICFP): 107:1-107:29 (2019) - [j41]Lau Skorstengaard, Dominique Devriese, Lars Birkedal:
StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities. Proc. ACM Program. Lang. 3(POPL): 19:1-19:28 (2019) - [j40]Ales Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal:
Iron: managing obligations in higher-order concurrent separation logic. Proc. ACM Program. Lang. 3(POPL): 65:1-65:30 (2019) - [i16]Lau Skorstengaard, Dominique Devriese, Lars Birkedal:
Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management - Technical Appendix Including Proofs and Details. CoRR abs/1902.05283 (2019) - [i15]Dan Frumin, Robbert Krebbers, Lars Birkedal:
Compositional Non-Interference for Fine-Grained Concurrent Programs. CoRR abs/1910.00905 (2019) - 2018
- [j39]Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer:
Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28: e20 (2018) - [j38]Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal:
A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST. Proc. ACM Program. Lang. 2(POPL): 64:1-64:28 (2018) - [j37]Ales Bizjak, Lars Birkedal:
A model of guarded recursion via generalised equilogical spaces. Theor. Comput. Sci. 722: 1-18 (2018) - [c88]Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg:
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. ESOP 2018: 214-241 - [c87]Lau Skorstengaard, Dominique Devriese, Lars Birkedal:
Reasoning About a Machine with Local Capabilities - Provably Safe Stack and Return Pointer Management. ESOP 2018: 475-501 - [c86]Dan Frumin, Robbert Krebbers, Lars Birkedal:
ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. LICS 2018: 442-451 - [c85]Aleksandr Karbyshev, Kasper Svendsen, Aslan Askarov, Lars Birkedal:
Compositional Non-interference for Concurrent Programs via Separation and Framing. POST 2018: 53-78 - [c84]Ales Bizjak, Lars Birkedal:
On Models of Higher-Order Separation Logic. MFPS 2018: 57-78 - [i14]Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg:
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. CoRR abs/1802.09787 (2018) - [i13]Lau Skorstengaard, Dominique Devriese, Lars Birkedal:
StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details. CoRR abs/1811.02787 (2018) - 2017
- [c83]Thomas Dinsdale-Young, Pedro da Rocha Pinto, Kristoffer Just Andersen, Lars Birkedal:
Caper - Automatic Verification for Fine-Grained Concurrency. ESOP 2017: 420-447 - [c82]Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal:
The Essence of Higher-Order Concurrent Separation Logic. ESOP 2017: 696-723 - [c81]Robbert Krebbers, Amin Timany, Lars Birkedal:
Interactive proofs in higher-order concurrent separation logic. POPL 2017: 205-217 - [c80]Morten Krogh-Jespersen, Kasper Svendsen, Lars Birkedal:
A relational model of types-and-effects in higher-order concurrent separation logic. POPL 2017: 218-231 - [i12]Lars Birkedal, Thomas Dinsdale-Young, Guilhem Jaber, Kasper Svendsen, Nikos Tzevelekos:
Trace Properties from Separation Logic Specifications. CoRR abs/1702.02972 (2017) - 2016
- [j36]Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, Lars Birkedal:
The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Log. Methods Comput. Sci. 12(3) (2016) - [j35]Lars Birkedal, Guilhem Jaber, Filip Sieczkowski, Jacob Thamsborg:
A Kripke logical relation for effect-based program transformations. Inf. Comput. 249: 160-189 (2016) - [j34]Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson, Kasper Svendsen, Lars Birkedal:
Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic. ACM Trans. Program. Lang. Syst. 38(2): 4:1-4:72 (2016) - [c79]Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi:
Guarded Cubical Type Theory: Path Equality for Guarded Recursion. CSL 2016: 23:1-23:17 - [c78]Kasper Svendsen, Filip Sieczkowski, Lars Birkedal:
Transfinite Step-Indexing: Decoupling Concrete and Logical Steps. ESOP 2016: 727-751 - [c77]Dominique Devriese, Lars Birkedal, Frank Piessens:
Reasoning about Object Capabilities with Logical Relations and Effect Parametricity. EuroS&P 2016: 147-162 - [c76]Ales Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus Ejlers Møgelberg, Lars Birkedal:
Guarded Dependent Type Theory with Coinductive Types. FoSSaCS 2016: 20-35 - [c75]Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer:
Higher-order ghost state. ICFP 2016: 256-269 - [c74]Lars Birkedal:
Preface. MFPS 2016: 1-2 - [e5]Lars Birkedal:
The Thirty-second Conference on the Mathematical Foundations of Programming Semantics, MFPS 2016, Carnegie Mellon University, Pittsburgh, PA, USA, May 23-26, 2016. Electronic Notes in Theoretical Computer Science 325, Elsevier 2016 [contents] - [i11]Ales Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus Ejlers Møgelberg, Lars Birkedal:
Guarded Dependent Type Theory with Coinductive Types. CoRR abs/1601.01586 (2016) - [i10]Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi:
Guarded Cubical Type Theory: Path Equality for Guarded Recursion. CoRR abs/1606.05223 (2016) - [i9]Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi:
Guarded Cubical Type Theory. CoRR abs/1611.09263 (2016) - 2015
- [c73]Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, Jean Pichon-Pharabod:
A Separation Logic for Fictional Sequential Consistency. ESOP 2015: 736-761 - [c72]Ales Bizjak, Lars Birkedal:
Step-Indexed Logical Relations for Probability. FoSSaCS 2015: 279-294 - [c71]Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, Lars Birkedal:
Programming and Reasoning with Guarded Recursion for Coinductive Types. FoSSaCS 2015: 407-421 - [c70]Filip Sieczkowski, Ales Bizjak, Lars Birkedal:
ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages. ITP 2015: 375-390 - [c69]Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer:
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. POPL 2015: 637-650 - [c68]Marco Paviotti, Rasmus Ejlers Møgelberg, Lars Birkedal:
A Model of PCF in Guarded Type Theory. MFPS 2015: 333-349 - [i8]Ales Bizjak, Lars Birkedal:
Step-Indexed Logical Relations for Probability (long version). CoRR abs/1501.02623 (2015) - [i7]Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, Lars Birkedal:
Programming and Reasoning with Guarded Recursion for Coinductive Types. CoRR abs/1501.02925 (2015) - [i6]Lars Birkedal, Derek Dreyer, Philippa Gardner, Zhong Shao:
Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191). Dagstuhl Reports 5(5): 1-23 (2015) - 2014
- [c67]Kasper Svendsen, Lars Birkedal:
Impredicative Concurrent Abstract Predicates. ESOP 2014: 149-168 - [c66]Lars Birkedal:
Modular reasoning about concurrent higher-order imperative programs. POPL 2014: 1-2 - [c65]Ales Bizjak, Lars Birkedal, Marino Miculan:
A Model of Countable Nondeterminism in Guarded Type Theory. RTA-TLCA 2014: 108-123 - 2013
- [j33]Lars Birkedal, Ales Bizjak, Jan Schwinghammer:
Step-Indexed Relational Reasoning for Countable Nondeterminism. Log. Methods Comput. Sci. 9(4) (2013) - [j32]Troels Christoffer Damgaard, Arne J. Glenstrup, Lars Birkedal, Robin Milner:
An inductive characterization of matching in binding bigraphs. Formal Aspects Comput. 25(2): 257-288 (2013) - [j31]Jan Schwinghammer, Lars Birkedal, François Pottier, Bernhard Reus, Kristian Støvring, Hongseok Yang:
A step-indexed Kripke model of hidden state. Math. Struct. Comput. Sci. 23(1): 1-54 (2013) - [c64]Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson:
Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library. ECOOP 2013: 327-351 - [c63]Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson:
Modular Reasoning about Separation of Concurrent Data Structures. ESOP 2013: 169-188 - [c62]Aaron Turon, Derek Dreyer, Lars Birkedal:
Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. ICFP 2013: 377-390 - [c61]Lars Birkedal, Rasmus Ejlers Møgelberg:
Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes. LICS 2013: 213-222 - [c60]Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, Hongseok Yang:
Views: compositional reasoning for concurrent programs. POPL 2013: 287-300 - [c59]Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, Derek Dreyer:
Logical relations for fine-grained concurrency. POPL 2013: 343-356 - 2012
- [j30]Jacob Thamsborg, Lars Birkedal, Hongseok Yang:
Two for the Price of One: Lifting Separation Logic Assertions. Log. Methods Comput. Sci. 8(3) (2012) - [j29]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. Log. Methods Comput. Sci. 8(4) (2012) - [j28]Derek Dreyer, Georg Neis, Lars Birkedal:
The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program. 22(4-5): 477-528 (2012) - [j27]Lars Birkedal, Kristian Støvring, Jacob Thamsborg:
A relational realizability model for higher-order stateful ADTs. J. Log. Algebraic Methods Program. 81(4): 491-521 (2012) - [c58]Lars Birkedal:
First Steps in Synthetic Guarded Domain Theory. Advances in Modal Logic 2012: 143 - [c57]Lars Birkedal, Filip Sieczkowski, Jacob Thamsborg:
A Concurrent Logical Relation. CSL 2012: 107-121 - [c56]Jonas Braband Jensen, Lars Birkedal:
Fictional Separation Logic. ESOP 2012: 377-396 - [c55]Jesper Bengtson, Jonas Braband Jensen, Lars Birkedal:
Charge! - A Framework for Higher-Order Separation Logic in Coq. ITP 2012: 315-331 - [c54]Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, Peter Sestoft:
Formalized Verification of Snapshotable Trees: Separation and Sharing. VSTTE 2012: 179-195 - [e4]Lars Birkedal:
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. Lecture Notes in Computer Science 7213, Springer 2012, ISBN 978-3-642-28728-2 [contents] - 2011
- [j26]Derek Dreyer, Amal Ahmed, Lars Birkedal:
Logical Step-Indexed Logical Relations. Log. Methods Comput. Sci. 7(2) (2011) - [j25]Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang:
Nested Hoare Triples and Frame Rules for Higher-order Store. Log. Methods Comput. Sci. 7(3) (2011) - [j24]Jonas Braband Jensen, Lars Birkedal, Peter Sestoft:
Modular Verification of Linked Lists with Views via Separation Logic. J. Object Technol. 10: 2: 1-20 (2011) - [c53]Jan Schwinghammer, Lars Birkedal:
Step-Indexed Relational Reasoning for Countable Nondeterminism. CSL 2011: 512-524 - [c52]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: 305-319 - [c51]Jacob Thamsborg, Lars Birkedal:
A kripke logical relation for effect-based program transformations. ICFP 2011: 445-456 - [c50]Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal:
Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq. ITP 2011: 22-38 - [c49]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: 55-64 - [c48]Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob Thamsborg, Hongseok Yang:
Step-indexed kripke models over recursive worlds. POPL 2011: 119-132 - [c47]Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski:
Partiality, State and Dependent Types. TLCA 2011: 198-212 - [c46]Alexandre Buisse, Lars Birkedal, Kristian Støvring:
Step-Indexed Kripke Model of Separation Logic for Storable Locks. MFPS 2011: 121-143 - 2010
- [j23]Lars Birkedal, Kristian Støvring, Jacob Thamsborg:
Realisability semantics of parametric polymorphism, general references and recursive types. Math. Struct. Comput. Sci. 20(4): 655-703 (2010) - [j22]Lars Birkedal, Kristian Støvring, Jacob Thamsborg:
The category-theoretic solution of recursive metric-space equations. Theor. Comput. Sci. 411(47): 4102-4122 (2010) - [c45]Jonas Braband Jensen, Lars Birkedal, Peter Sestoft:
Modular verification of linked lists with views via separation logic. FTfJP@ECOOP 2010: 4:1-4:7 - [c44]Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson:
Verifying Generics and Delegates. ECOOP 2010: 175-199 - [c43]Lars Birkedal, Jan Schwinghammer, Kristian Støvring:
A Metric Model of Lambda Calculus with Guarded Recursion. FICS 2010: 19-25 - [c42]Lars Birkedal, Jan Schwinghammer, Kristian Støvring:
A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces. FICS 2010: 27-33 - [c41]Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, Bernhard Reus:
A Semantic Foundation for Hidden State. FoSSaCS 2010: 2-17 - [c40]Derek Dreyer, Georg Neis, Lars Birkedal:
The impact of higher-order state and control effects on local relational reasoning. ICFP 2010: 143-156 - [c39]Derek Dreyer, Georg Neis, Andreas Rossberg, Lars Birkedal:
A relational modal logic for higher-order stateful ADTs. POPL 2010: 185-198 - [c38]Neel Krishnaswami, Lars Birkedal, Jonathan Aldrich:
Verifying event-driven programs using ramified frame properties. TLDI 2010: 63-76 - [e3]Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann:
Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010. Dagstuhl Seminar Proceedings 10351, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany 2010 [contents] - [i5]Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann:
10351 Abstracts Collection - Modelling, Controlling and Reasoning About State. Modelling, Controlling and Reasoning About State 2010 - [i4]Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann:
10351 Executive Summary - Modelling, Controlling and Reasoning About State. Modelling, Controlling and Reasoning About State 2010
2000 – 2009
- 2009
- [c37]Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang:
Nested Hoare Triples and Frame Rules for Higher-Order Store. CSL 2009: 440-454 - [c36]Lars Birkedal, Kristian Støvring, Jacob Thamsborg:
Solutions of Generalized Recursive Metric-Space Equations. FICS 2009: 18-24 - [c35]Lars Birkedal, Kristian Støvring, Jacob Thamsborg:
Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types. FoSSaCS 2009: 456-470 - [c34]Derek Dreyer, Amal Ahmed, Lars Birkedal:
Logical Step-Indexed Logical Relations. LICS 2009: 71-80 - [c33]Lars Birkedal, Kristian Støvring, Jacob Thamsborg:
Relational parametricity for references and recursive types. TLDI 2009: 91-104 - [c32]Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal, Kasper Svendsen, Alexandre Buisse:
Design patterns in separation logic. TLDI 2009: 105-116 - 2008
- [j21]Rasmus Ejlers Møgelberg, Lars Birkedal, Giuseppe Rosolini:
Synthetic domain theory and models of linear Abadi & Plotkin logic. Ann. Pure Appl. Log. 155(2): 115-133 (2008) - [j20]Aleksandar Nanevski, J. Gregory Morrisett, Lars Birkedal:
Hoare type theory, polymorphism and separation. J. Funct. Program. 18(5-6): 865-911 (2008) - [j19]Lars Birkedal, Hongseok Yang:
Relational Parametricity and Separation Logic. Log. Methods Comput. Sci. 4(2) (2008) - [j18]Noah Torp-Smith, Lars Birkedal, John C. Reynolds:
Local reasoning about a copying garbage collector. ACM Trans. Program. Lang. Syst. 30(4): 24:1-24:58 (2008) - [c31]Lars Birkedal, Søren Debois, Thomas T. Hildebrandt:
On the Construction of Sorted Reactive Systems. CONCUR 2008: 218-232 - [c30]Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett:
A Realizability Model for Impredicative Hoare Type Theory. ESOP 2008: 337-352 - [c29]Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Hongseok Yang:
A Simple Model of Separation Logic for Higher-Order Store. ICALP (2) 2008: 348-360 - [c28]Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal:
Ynot: dependent types for imperative programs. ICFP 2008: 229-240 - [c27]Carsten Varming, Lars Birkedal:
Higher-Order Separation Logic in Isabelle/HOLCF. MFPS 2008: 371-389 - [i3]Lars Birkedal, Hongseok Yang:
Relational Parametricity and Separation Logic. CoRR abs/0805.0783 (2008) - 2007
- [j17]Lars Birkedal:
Book Reviews. Stud Logica 86(1): 133-135 (2007) - [j16]Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen:
Domain-theoretical models of parametric polymorphism. Theor. Comput. Sci. 388(1-3): 152-172 (2007) - [j15]Bodil Biering, Lars Birkedal, Noah Torp-Smith:
BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst. 29(5): 24 (2007) - [c26]Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal:
Abstract Predicates and Mutable ADTs in Hoare Type Theory. ESOP 2007: 189-204 - [c25]Lars Birkedal, Hongseok Yang:
Relational Parametricity and Separation Logic. FoSSaCS 2007: 93-107 - 2006
- [j14]Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen:
Linear Abadi and Plotkin Logic. Log. Methods Comput. Sci. 2(5) (2006) - [j13]Lars Birkedal, Noah Torp-Smith, Hongseok Yang:
Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages. Log. Methods Comput. Sci. 2(5) (2006) - [j12]Troels Christoffer Damgaard, Lars Birkedal:
Axiomatizing Binding Bigraphs. Nord. J. Comput. 13(1-2): 58-77 (2006) - [c24]Nina Bohr, Lars Birkedal:
Relational Reasoning for Recursive Types and References. APLAS 2006: 79-96 - [c23]Lars Birkedal, Søren Debois, Thomas T. Hildebrandt:
Sortings for Reactive Systems. CONCUR 2006: 248-262 - [c22]Lars Birkedal, Søren Debois, Ebbe Elsborg, Thomas T. Hildebrandt, Henning Niss:
Bigraphical Models of Context-Aware Systems. FoSSaCS 2006: 187-201 - [c21]Aleksandar Nanevski, Greg Morrisett, Lars Birkedal:
Polymorphism and separation in hoare type theory. ICFP 2006: 62-73 - [c20]Lars Birkedal, Troels Christoffer Damgaard, Arne J. Glenstrup, Robin Milner:
Matching of Bigraphs. GT-VC@CONCUR 2006: 3-19 - [i2]Lars Birkedal, Noah Torp-Smith, Hongseok Yang:
Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages. CoRR abs/cs/0610081 (2006) - [i1]Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen:
Linear Abadi and Plotkin Logic. CoRR abs/cs/0611004 (2006) - 2005
- [j11]Lars Birkedal, Rasmus Ejlers Møgelberg:
Categorical models for Abadi and Plotkin's logic for parametricity. Math. Struct. Comput. Sci. 15(4): 709-772 (2005) - [c19]Bodil Biering, Lars Birkedal, Noah Torp-Smith:
BI Hyperdoctrines and Higher-Order Separation Logic. ESOP 2005: 233-247 - [c18]Lars Birkedal, Noah Torp-Smith, Hongseok Yang:
Semantics of Separation-Logic Typing and Higher-Order Frame Rules. LICS 2005: 260-269 - [c17]Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen:
Parametric Domain-theoretic Models of Polymorphic Intuitionistic / Linear Lambda Calculus. MFPS 2005: 191-217 - [c16]Rasmus Ejlers Møgelberg, Lars Birkedal, Giuseppe Rosolini:
Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic. MFPS 2005: 219-245 - [e2]Lars Birkedal:
Proceedings of the 10th Conference on Category Theory in Computer Science, CTCS 2004, Copenhagen, Denmark, August 12-14, 2004. Electronic Notes in Theoretical Computer Science 122, Elsevier 2005 [contents] - 2004
- [j10]Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg:
A Retrospective on Region-Based Memory Management. High. Order Symb. Comput. 17(3): 245-265 (2004) - [j9]Andrej Bauer, Lars Birkedal, Dana S. Scott:
Equilogical spaces. Theor. Comput. Sci. 315(1): 35-59 (2004) - [j8]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. 316(1): 1-2 (2004) - [c15]J. Aa. Serensen, Kåre J. Kristoffersen, Andres Cervera, M. Schiortz, Thomas Lynge, Zoltan Safar, Lars Birkedal:
An infrastructure for context dependent mobile multimedia communication. MMSP 2004: 462-465 - [c14]Lars Birkedal, Noah Torp-Smith, John C. Reynolds:
Local reasoning about a copying garbage collector. POPL 2004: 220-231 - [c13]Lars Birkedal:
Preface. CTCS 2004: 1- - 2002
- [j7]Lars Birkedal, Jaap van Oosten:
Relative and modified relative realizability. Ann. Pure Appl. Log. 118(1-2): 115-132 (2002) - [j6]Lars Birkedal:
A general notion of realizability. Bull. Symb. Log. 8(2): 266-282 (2002) - [j5]Steven Awodey, Lars Birkedal, Dana S. Scott:
Local Realizability Toposes and a Modal Logic for Computability. Math. Struct. Comput. Sci. 12(3): 319-334 (2002) - 2001
- [j4]Lars Birkedal, Mads Tofte:
A constraint-based region inference algorithm. Theor. Comput. Sci. 258(1-2): 299-392 (2001) - 2000
- [b1]Lars Birkedal:
Developing Theories of Types and Computability via Realizability. Electronic Notes in Theoretical Computer Science 34, Elsevier 2000, pp. 1-282 - [c12]Mads Tofte, Lars Birkedal:
Unification and polymorphism in region inference. Proof, Language, and Interaction 2000: 389-424 - [c11]Andrej Bauer, Lars Birkedal:
Continuous Functionals of Dependent Types and Equilogical Spaces. CSL 2000: 202-216 - [c10]Lars Birkedal:
A General Notion of Realizability. LICS 2000: 7-17
1990 – 1999
- 1999
- [j3]Lars Birkedal, Robert Harper:
Relational Interpretations of Recursive Types in an Operational Setting. Inf. Comput. 155(1-2): 3-63 (1999) - [c9]Steven Awodey, Lars Birkedal, Dana S. Scott:
Local Realizability Toposes and a Modal Logic for Computability. Realizability Semantics and Applications@FLoC 1999: 13-26 - [c8]Lars Birkedal:
Bibliography on Realizability. Realizability Semantics and Applications@FLoC 1999: 40-57 - [c7]Lars Birkedal, Jaap van Oosten, Giuseppe Rosolini, Dana S. Scott:
Preface. Realizability Semantics and Applications@FLoC 1999: 189-190 - [e1]Lars Birkedal, Jaap van Oosten, Giuseppe Rosolini, Dana S. Scott:
Tutorial Workshop on Realizability Semantics and Applications, associated to FLoC'99, the 1999 Federated Logic Conference, Trento, Italy, June 30 - July 1, 1999. Electronic Notes in Theoretical Computer Science 23(1), Elsevier 1999 [contents] - 1998
- [j2]Mads Tofte, Lars Birkedal:
A Region Inference Algorithm. ACM Trans. Program. Lang. Syst. 20(4): 724-767 (1998) - [c6]Lars Birkedal, Aurelio Carboni, Giuseppe Rosolini, Dana S. Scott:
Type Theory via Exact Categories. LICS 1998: 188-198 - [c5]Lars Birkedal:
On propositions-as-types in realizability models. Workshop on Domains 1998: 52 - 1997
- [c4]Lars Birkedal, Robert Harper:
Relational Interpretations of Recursive Types in an operational Setting (Summary). TACS 1997: 458-490 - 1996
- [c3]Lars Birkedal, Mads Tofte, Magnus Vejlstrup:
From Region Inference to von Neumann Machines via Region Representation Inference. POPL 1996: 171-183 - 1995
- [j1]Lars Birkedal, Morten Welinder:
Binding-Time Analysis for Standard ML. LISP Symb. Comput. 8(3): 191-208 (1995) - 1994
- [c2]Lars Birkedal, Morten Welinder:
Binding-Time Analysis for Standard ML. PEPM 1994: 61-71 - [c1]Lars Birkedal, Morten Welinder:
Hand-Writing Program Generator Generators. PLILP 1994: 198-214
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-12 20:59 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
