Simon Oddershede Gregersen

I am no longer affiliated with Aarhus University and may loose access to this homepage. Please continue to my personal website at https://simongregersen.com.

I am a postdoctoral fellow in the Computer Science Department at the Courant Institute of Mathematical Sciences of New York University. I am advised by 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 proving properties of distributed systems and randomized programs.

My research 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

Publications

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages
PDF Extended version Coq development Slides

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Léon Gondelman, Abel Nieto, and Lars 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
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, and Lars 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éon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, and Lars 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
Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, and Lars Birkedal
In ESOP 2020: European Symposium on Programming
PDF Talk Technical appendix Coq development Slides

A Dependently Typed Library for Static Information-Flow Control in Idris
Simon Oddershede Gregersen, Søren Eller Thomsen, and Aslan 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 Jul 2023
Slides

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Contributed talk at VeriProP, 17 Jul 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 Nov 2020
Slides