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

orcid.svg github.svg scholar.svg dblp.svg

Preprints

Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
Submitted for publication
arXiv

Publications

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

Validate