Toggle navigation
Sign in
Sign up
conf.researchr.org
/
Lars Birkedal
conf.researchr.org general profile
ESOP 2015 profile
ETAPS 2019 profile
ICFP 2016 profile
ICFP 2018 profile
ICFP 2019 profile
ICFP 2020 profile
ICFP 2021 profile
ICFP 2022 profile
PLDI 2021 profile
PLDI 2022 profile
POPL 2017 profile
POPL 2018 profile
POPL 2019 profile
POPL 2020 profile
POPL 2021 profile
POPL 2022 profile
POPL 2023 profile
SPLASH 2022 profile
Registered user since Wed 15 Feb 2017
Name:
Lars Birkedal
Country:
Denmark
Affiliation:
Aarhus University
Personal website:
http://cs.au.dk/~birke/
Contributions
POPL 2023
Author of Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice within the POPL-track
SPLASH 2022
Committee Member in Review Committee within the OOPSLA-track
Author of Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities within the OOPSLA-track
Author of Modular Verification of Op-Based CRDTs in Separation Logic within the V-OOPSLA-track
ICFP 2022
Committee Member in Program Committee within the ICFP Papers and Events-track
Author of Later Credits: Resourceful Reasoning for the Later Modality within the ICFP Papers and Events-track
PLDI 2022
Author of (PLDI 2021) Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic within the SIGPLAN Track-track
WITS 2022
Author of mitten: A Flexible Multimodal Proof Assistant within the WITS 2022-track
CPP 2022
Committee Member in Program Committee within the CPP 2022-track
Author of Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library within the CPP 2022-track
ICFP 2021
Author of Theorems for Free from Separation Logic Specifications within the Research Papers-track
Author of Client-Server Sessions in Linear Logic within the Research Papers-track
PLDI 2021
Author of Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic within the PLDI-track
POPL 2021
Author of Efficient and Provable Local Capability Revocation using Uninitialized Capabilities within the POPL-track
Author of Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic within the POPL-track
Author of Mechanized Logical Relations for Termination-Insensitive Noninterference within the POPL-track
CPP 2021
Author of Reasoning About Monotonicity in Separation Logic within the CPP 2021-track
Author of Contextual Refinement of the Michael-Scott Queue (Proof Pearl) within the CPP 2021-track
PriSC 2021
Author of Toward Complete Stack Safety for Capability Machines within the PriSC 2021-track
ICFP 2020
Author of Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris within the ICFP Program-track
POPL 2020
Session Chair of Automatic Differentiation / Kleene Algebra (part of Research Papers)
Program Chair in Organizing Committee
PC Chair in Program Committee within the Research Papers-track
Session Chair of Invited Talk (part of Research Papers)
Session Chair of Welcome + SIGPLAN Award Ceremony (part of Research Papers)
PriSC 2020
Author of Mechanized Reasoning about a Capability Machine within the Principles of Secure Compilation 2020-track
ICFP 2019
Author of Mechanized Relational Verification of Concurrent Programs with Continuations within the Research Papers-track
Author of Implementing a Modal Dependent Type Theory within the Research Papers-track
ESOP 2019
Committee Member in Program Committee within the ESOP 2019-track
POPL 2019
Author of StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities within the Research Papers-track
Author of Iron: Managing Obligations in Higher-Order Concurrent Separation Logic within the Research Papers-track
Presenter of POPL 2020 Announcement within the Research Papers-track
PriSC 2019
Committee Member in Program Committee within the PriSC 2019-track
ICFP 2018
Committee Member in External Review Committee within the Research Papers-track
POPL 2018
Author of A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST within the Research Papers-track
Author of A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST within the Artifact Evaluation-track
Session Chair of Probability (part of Research Papers)
Session Chair of Outside the box (part of Research Papers)
Committee Member in Program Committee within the Research Papers-track
PriSC 2018
Committee Member in Program Committee within the PriSC 2018-track
Session Chair of Session 3 (part of PriSC 2018)
Author of Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities within the PriSC 2018-track
POPL 2017
ERC member in External Review Committee within the POPL-track
Author of Interactive Proofs in Higher-Order Concurrent Separation Logic within the POPL-track
Session Chair of Semantic Foundations (part of POPL)
Author of A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic within the POPL-track
CoqPL 2017
Author of Logical Relations in Iris within the CoqPL 2017-track
ICFP 2016
Committee Member in External Review Committee within the Research Papers-track
Author of Higher-Order Ghost State within the Research Papers-track
HOPE 2016
Co-chair in Program Committee within the HOPE-track
Author of A Logical Account of a Type-and-Effect System within the HOPE-track
Author of Opening remarks within the HOPE-track
ESOP 2015
Session Chair of Session 4 (part of ESOP)
Committee Member in Program Committee within the ESOP-track
Author of A Separation Logic for Fictional Sequential Consistency within the ESOP-track
Share
x
Mon 6 Feb 07:05