Simon Oddershede Gregersen
I am a postdoctoral researcher at the Courant Institute of New York University, working with Joseph Tassarotti. I received my PhD from Aarhus University in 2023 under the guidance of Amin Timany and Lars Birkedal.
My research focuses on programming languages and program verification, in particular for security properties, distributed systems, and randomized programs. Specifically, I work on techniques to develop formally verified software systems that come with machine-checked mathematical proofs. I devise and apply new techniques, such as separation logics and logical relations, that make it feasible or easier to construct such proofs.
My work is currently supported by an Internationalization Fellowship from the Carlsberg Foundation (CF23-0791).
In January 2026, I will start as a tenure-track faculty at CISPA. I will be recruiting interns, PhD students, and postdocs. If you might be interested, I encourage you to reach out.
Contact
E-mail: s.gregersen@nyu.edu
CV (April 2025)
Preprints
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
arXiv
Publications
Logical Relations for Formally Verified Authenticated Data Structures
Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti
To appear in CCS 2025: ACM SIGSAC Conference on Computer and Communications Security
PDF arXiv Artifact Rocq development
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
In POPL 2025: ACM SIGPLAN Symposium on Principles of Programming Languages
PDF DOI arXiv Artifact Rocq development
Tachis: Higher-Order Separation Logic with Credits for Expected Costs
Phillipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
In OOPSLA 2024: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications
PDF DOI arXiv Artifact Rocq development
Almost-Sure Termination by Guarded Refinement
Simon Oddershede Gregersen, Alejandro Aguirre, Phillipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
In ICFP 2024: ACM SIGPLAN International Conference on Functional Programming
PDF DOI arXiv Artifact Rocq development Slides Talk
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
Alejandro Aguirre, Phillipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
In ICFP 2024: ACM SIGPLAN International Conference on Functional Programming
Recipient of the ICFP 2024 Distinguished Paper Award
PDF DOI arXiv Artifact Rocq development Talk
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Simon Oddershede Gregersen, Alejandro Aguirre, Phillipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages
PDF DOI arXiv Artifact Rocq development Slides Talk
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas K. Hinrichsen, Léon Gondelman, Abel Nieto, Lars Birkedal
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages
PDF DOI arXiv Rocq development
Mechanized Logical Relations for Termination-Insensitive Noninterference
Simon Oddershede Gregersen, Johan Bay, Amin Timany, Lars Birkedal
In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
PDF DOI Technical appendix Rocq development Slides
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, Lars Birkedal
In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
PDF DOI Technical appendix Rocq development
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
Morten Krogh-Jespersen, Amin Timany, Marit E. Ohlenbusch, Simon Oddershede Gregersen, Lars Birkedal
In ESOP 2020: European Symposium on Programming
PDF DOI Technical appendix Rocq development Slides Talk
A Dependently Typed Library for Static Information-Flow Control in Idris
Simon Oddershede Gregersen, Søren E. Thomsen, Aslan Askarov
In POST 2019: Principles of Security and Trust
PDF DOI Extended version Idris development
Dissertation
Selected talks
Logical Relations for Formally Verified Authenticated Data Structures
Contributed talk at The Iris Workshop, 2 June 2025
Slides
Logical Relations for Formally Verified Authenticated Data Structures
Contributed talk at the New Jersey Programming Languages and Systems Seminar, 9 May, 2025
Slides
Logical Relations for Formally Verified Authenticated Data Structures
Invited talk at the VU Amsterdam PLSec reading group, 16 April, 2025
Slides
Trillium: Intensional Refinement in Higher-Order Separation Logic
Contributed talk at New England Systems Verification Day, 26 April 2024
Slides
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Invited seminar at the Bristol Programming Languages Research group seminar, 19 July 2023
Slides
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Contributed talk at VeriProP, 17 July 2023
Slides
Trillium: History-Sensitive Refinement in Separation Logic
Contributed talk at The Iris Workshop, 3 May 2022
Slides
Mechanized Logical Relations for Termination-Insensitive Noninterference
Invited seminar at the Chalmers ProgLog/Security seminar, 4 November 2020
Slides