Simon Oddershede Gregersen

I am a postdoctoral fellow in the Computer Science Department at the Courant Institute of Mathematical Sciences of New York University. I am hosted and advised by Joseph Tassarotti. I obtained my PhD from Aarhus University in 2023 where I was advised by Amin Timany and Lars Birkedal.

I study programming languages and program verification. I am particularly interested in techniques for proving properties of distributed systems and randomized programs.

My work is currently funded by a Carlsberg Internationalization Fellowship (CF23-0791).

Contact

E-mail: s.gregersen@nyu.edu
Office: Room 406, 60 Fifth Avenue, New York, NY 10011

orcid.svg github.svg scholar.svg

Preprints

Almost-Sure Termination by Guarded Refinement
S. O. Gregersen, A. Aguirre, P. G. Haselwarter, J. Tassarotti, and L. Birkedal
Submitted for publication
PDF

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
A. Aguirre, P. G. Haselwarter, M. de Medeiros, K. H. Li, S. O. Gregersen, J. Tassarotti, and L. Birkedal
Submitted for publication
PDF

Publications

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
S. O. Gregersen, A. Aguirre, P. G. Haselwarter, J. Tassarotti, and L. Birkedal
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages
PDF Extended version Coq development Slides Talk

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
A. Timany, S. O. Gregersen, L. Stefanesco, J. K. Hinrichsen, L. Gondelman, A. Nieto, and L. Birkedal
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages
PDF Extended version Coq development

Higher-Order Separation Logic for Distributed Systems and Security
S. O. Gregersen
PhD dissertation, Aarhus University, March 2023
PDF Slides

Mechanized Logical Relations for Termination-Insensitive Noninterference
S. O. Gregersen, J. Bay, A. Timany, and L. Birkedal
In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
PDF Technical appendix Coq development Slides

Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
L. Gondelman, S. O. Gregersen, A. Nieto, A. Timany, and L. Birkedal
In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
PDF Technical appendix Coq development

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
M. Krogh-Jespersen, A. Timany, M. E. Ohlenbusch, S. O. Gregersen, and L. Birkedal
In ESOP 2020: European Symposium on Programming
PDF Technical appendix Coq development Slides Talk

A Dependently Typed Library for Static Information-Flow Control in Idris
S. O. Gregersen, S. E. Thomsen, and A. Askarov
In POST 2019: Principles of Security and Trust
PDF Extended version Idris development

Selected talks

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