Simon Oddershede Gregersen
Tenure-Track Faculty, CISPA Helmholtz Center for Information Security
Hi there! My name is Simon and I am tenure-track faculty at CISPA. I study programming languages and program verification. I develop and apply new techniques that make it feasible or easier to build software systems with formal guarantees of correctness and security. Currently, my work revolves around distributed and randomized systems and techniques such as program logics, separation logic, logical relations, type systems, and interactive theorem provers.
Before joing CISPA, I was a postdoctoral fellow at New York University with Joseph Tassarotti. I received my PhD from Aarhus University, supervised by Amin Timany and Lars Birkedal.
If you are interested in internships, a PhD, or a postdoc with me, I encourage you to reach out.
Contact: [email protected]
CV (January 2026)
Preprints
Building Extensible Program Logics through Effect Handlers
Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti
Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic
Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
Publications
Logical Relations for Formally Verified Authenticated Data Structures ccs 2025
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs icfp 2025
Approximate Relational Reasoning for Higher-Order Probabilistic Programs popl 2025
Tachis: Higher-Order Separation Logic with Credits for Expected Costs oopsla 2024
Almost-Sure Termination by Guarded Refinement icfp 2024
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs icfp 2024
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic popl 2024
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement popl 2024
Mechanized Logical Relations for Termination-Insensitive Noninterference popl 2021
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic popl 2021
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems esop 2020
A Dependently Typed Library for Static Information-Flow Control in Idris post 2019
Simon Oddershede Gregersen, Søren E. Thomsen, Aslan Askarov
Dissertation
Selected Miscellaneous Talks
- Logical Relations for Formally Verified Authenticated Data Structures
- New England Systems Verification Day, 3 October, 2025
Iris Workshop, 2 June 2025
New Jersey Programming Languages and Systems Seminar, 9 May, 2025
VU Amsterdam PLSec reading group, 16 April, 2025 - Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
- New England Systems Verification Day, 26 April 2024
Iris Workshop, 3 May 2022 - Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
- Bristol Programming Languages Research group seminar, 19 July 2023
VeriProP, 17 July 2023 - Mechanized Logical Relations for Termination-Insensitive Noninterference
- Chalmers ProgLog/Security seminar, 4 November 2020