Lars Birkedal -

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