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 supervised 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 formal techniques for proving properties of distributed systems and randomized programs.
My work is currently funded by a Internationalization Fellowship from the Carlsberg Foundation (CF23-0791).
Contact
E-mail: s.gregersen@nyu.edu
Office: 406, 60 Fifth Avenue, New York, NY 10011
Preprints
Tachis: Higher-Order Separation Logic with Credits for Expected Costs
Phillipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon O. Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
Accepted for publication at OOPSLA 2024
arXiv
Almost-Sure Termination by Guarded Refinement
Simon O. Gregersen, Alejandro Aguirre, Phillipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal
Accepted for publication at ICFP 2024
arXiv
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
Alejandro Aguirre, Phillipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon O. Gregersen, Joseph Tassarotti, and Lars Birkedal
Accepted for publication at ICFP 2024
arXiv
Publications
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Simon O. Gregersen, Alejandro Aguirre, Phillipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages
PDF DOI Extended version Coq development Slides Talk
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
Amin Timany, Simon O. Gregersen, Léo Stefanesco, Jonas K. Hinrichsen, Léon Gondelman, Abel Nieto, and Lars Birkedal
In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages
PDF DOI Extended version Coq development
Higher-Order Separation Logic for Distributed Systems and Security
Simon O. Gregersen
PhD dissertation, Aarhus University, March 2023
PDF Slides
Mechanized Logical Relations for Termination-Insensitive Noninterference
Simon O. Gregersen, Johan Bay, Amin Timany, and 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 O. Gregersen, Abel Nieto, Amin Timany, and 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 O. Gregersen, and 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 O. Gregersen, Søren E. Thomsen, and 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