Lars Birkedal

Registered user since Wed 15 Feb 2017

Name:Lars Birkedal
Affiliation:Aarhus University
Personal website:http://cs.au.dk/~birke/

Contributions

ICFP 2022 Committee Member in Program Committee within the ICFP Papers-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
PriSC 2021 Author of Toward Complete Stack Safety for Capability Machines within the PriSC 2021-track
PLDI 2021 Author of Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic within the PLDI-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
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
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
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
PriSC 2020 Author of Mechanized Reasoning about a Capability Machine within the Principles of Secure Compilation 2020-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 2019 Committee Member in Program Committee within the PriSC 2019-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
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
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
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
CoqPL 2017 Author of Logical Relations in Iris within the CoqPL 2017-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
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
ICFP 2016 Committee Member in External Review Committee within the Research Papers-track
Author of Higher-Order Ghost State within the Research Papers-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