Simon Oddershede Gregersen
I am a postdoctoral fellow in the Computer Science Department at the Courant Institute of New York University, working with Joseph Tassarotti. I obtained my PhD from Aarhus University in 2023 under supervision of Amin Timany and Lars Birkedal.
I study programming languages and program verification. I am particularly interested in formal techniques for proving properties of distributed systems and randomized programs.
My work is currently supported by an Internationalization Fellowship from the Carlsberg Foundation (CF23-0791).
Contact
E-mail: s.gregersen@nyu.edu
Office: 406, 60 Fifth Avenue, New York, NY 10011
Publications
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 arXiv Artifact Coq 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 Coq 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 Coq 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 Coq 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 Coq 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 Coq development
Higher-Order Separation Logic for Distributed Systems and Security
Simon Oddershede Gregersen
PhD dissertation, Aarhus University, March 2023
PDF Slides
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 Coq 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 Coq 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 Coq 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
Selected talks
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