Simon Oddershede Gregersen
Simon Oddershede Gregersen
I am a postdoctoral researcher in the Logic and Semantics group at Aarhus University. I earned my Ph.D. from Aarhus University in March 2023 under the supervision of Lars Birkedal.
I study programming languages and program verification through the lens of higher-order separation logic.
Contact
Unpublished Manuscripts
Asynchronous Probabilistic Couplings in Higher-Order Separation Logics
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal
2023
Preprint Coq development
Trillium: History-Sensitive Refinement in Separation Logic
Amin Timany, Simon Oddershede Gregersen, L. Stefanesco, L. Gondelman, A. Nieto, and Lars Birkedal
2022
Preprint Coq development
Publications
Higher-Order Separation Logic for Distributed Systems and Security
Simon Oddershede Gregersen
Ph.D. dissertation, Aarhus University, March 2023
PDF
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
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
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
Teaching
- Teaching assistant for Compilation with Aslan Askarov (BSc course, 2020)
- Guest lecturer in Program Analysis and Verification (MSc course, 2019) on Concurrency and Invariants
- Guest lecturer in Language-Based Security (MSc course, 2019) on Spectre and Meltdown
- Teaching assistant for Programming Languages with Anders Møller (BSc course, 2018, 2019, 2022)
- Teaching assistant for Functional Programming with Bas Spitters (MSc course, 2018)
Work Experience
- Student programmer at Center for Advanced Software Analysis, Aarhus University, 2017
- Student software developer at CCI Europe A/S (now Stibo DX), Aarhus, 2015 - 2017