Simon Oddershede Gregersen
Postdoctoral Fellow, New York University
Hi there! My name is Simon. I will be joining CISPA as tenure-track faculty in January 2026. Until then, I am a postdoctoral fellow at New York University with Joseph Tassarotti. I received my PhD from Aarhus University in 2023, supervised by Amin Timany and Lars Birkedal.
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.
My work is supported by a fellowship from the Carlsberg Foundation (CF23-0791).
If you are interested in collaborating, an internship, or a PhD with me, I encourage you to reach out.
Contact: s.gregersen@nyu.edu
CV (October 2025)
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
- Contributed talk at New England Systems Verification Day, 3 October, 2025
Contributed talk at The Iris Workshop, 2 June 2025
Contributed talk at the New Jersey Programming Languages and Systems Seminar, 9 May, 2025
Invited talk at the VU Amsterdam PLSec reading group, 16 April, 2025 - Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
- Contributed talk at New England Systems Verification Day, 26 April 2024
Contributed talk at The Iris Workshop, 3 May 2022 - Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
- Invited talk at the Bristol Programming Languages Research group seminar, 19 July 2023
Contributed talk at VeriProP, 17 July 2023 - Mechanized Logical Relations for Termination-Insensitive Noninterference
- Invited talk at the Chalmers ProgLog/Security seminar, 4 November 2020