Simon Oddershede Gregersen

Simon Oddershede Gregersen


I am a PhD student in the Logic and Semantics group in the Department of Computer Science at Aarhus University. I am advised by Lars Birkedal.

I study programming languages, language-based security, and logics. I am particularly interested in developing foundations of compositional formal methods for establishing correctness and security of implementations of concurrent and distributed systems.

Publications

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, Virtual, Denmark
PDF Technical appendix Coq development

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, Virtual, Denmark
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, Dublin, Ireland
PDF Technical appendix Coq development

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, Prague, Czech Republic
PDF Extended version Idris development

Teaching

  • Teaching assistant for Compilation under 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 under Anders Møller (BSc course, 2018 & 2019)
  • Teaching assistant for Functional Programming under Bas Spitters (MSc course, 2018)

Work Experience

Created: 2020-12-16 Wed 09:25

Validate