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