معرفی
Lars Birkedal is a Professor of Computer Science at Aarhus University, Denmark, where he serves as Head of the Logic and Semantics Group. He previously held positions at the IT University of Copenhagen until 2012 and served as Head of Department of Computer Science at Aarhus from 2014 to 2017.
His educational background includes a Ph.D. in Computer Science from Carnegie Mellon University, USA, completed in December 1999.
Birkedal's primary research interests focus on the logic and semantics of programming languages and type theories. His current work centers on program logics for reasoning about distributed, concurrent, higher-order, and imperative programs; cyber-security; and type theories with guarded recursion. He has made significant contributions to separation logic, particularly through the development of the Iris framework, which earned him the 2023 Alonzo Church Award. His research bridges theoretical foundations with practical applications in program verification and security.
His recent publications demonstrate a strong trend toward mechanized verification of complex systems, with particular emphasis on concurrent and distributed programming. The research spans multiple subfields including separation logic variants, capability systems, information flow security, and formal verification of low-level systems. A notable pattern is the integration of logical frameworks with practical verification tools, often implemented in proof assistants like Coq.
His scientific achievements have been recognized with numerous prestigious awards:
- Fellow of the ACM
- ERC Advanced Grant from the European Research Council (2023)
- 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation
- Villum Investigator grant from the Villum Foundation (2019)
- Danish Minister of Research Elite Research Award (2015)
- Sapere Aude Advanced Grant from the Danish National Science Research Council (2013)
- ACM SIGPLAN Milner Award (2013)
Birkedal has advised numerous PhD students and postdocs, including Lau Skorstengaard, Kristoffer Just Andersen, Morten Krogh-Jespersen, and Robbert Krebbers. His research has been supported by significant grants including an ERC Advanced Grant (2023), a Villum Investigator grant (2019), and a Sapere Aude Advanced Grant (2013). He has served in editorial roles including Editor-in-Chief of Logical Methods in Computer Science (2014-2020) and Chairman of the board, and as PC Chair for POPL 2020.
He leads the Logic and Semantics Group at Aarhus University and has been instrumental in several major research projects including the CHORDS project (Compositional Higher-Order Reasoning about Distributed Systems) and the Center for Basic Research in Program Verification (CPV). His earlier ModuRes project (Modular Reasoning about Concurrent Higher-Order Imperative Programs) laid important groundwork for verification of modern programming language features.
