Lars Birkedal

Registered user since Wed 15 Feb 2017

Name: Lars Birkedal

Affiliation: Aarhus University

Personal website: http://cs.au.dk/~birke/

Contributions

PriSC 2021 Author of Toward Complete Stack Safety for Capability Machines within the PriSC 2021-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
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