A Dependently Typed Library for Static Information-Flow Control in Idris. - Simon Oddershede Gregersen; Søren Eller Thomsen; Aslan Askarov (POST, 2019)

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. - Morten Krogh-Jespersen; Amin Timany; Marit Edna Ohlenbusch; Simon Oddershede Gregersen; Lars Birkedal (ESOP, 2020)

Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic. - Amin Timany; Simon Oddershede Gregersen; Léo Stefanesco; Léon Gondelman; Abel Nieto; Lars Birkedal (CoRR, 2021)

Distributed causal memory: modular specification and verification in higher-order distributed separation logic. - Léon Gondelman; Simon Oddershede Gregersen; Abel Nieto; Amin Timany; Lars Birkedal (Proc. ACM Program. Lang., 2021)

Mechanized logical relations for termination-insensitive noninterference. - Simon Oddershede Gregersen; Johan Bay; Amin Timany; Lars Birkedal (Proc. ACM Program. Lang., 2021)

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic - Coq Artifact. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Zenodo, 2023)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement - Coq Artifact. - Amin Timany; Simon Oddershede Gregersen; Léo Stefanesco; Jonas Kastberg Hinrichsen; Léon Gondelman; Abel Nieto; Lars Birkedal (Zenodo, 2023)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. - Alejandro Aguirre 001; Philipp G. Haselwarter; Markus de Medeiros; Kwing Hei Li; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Almost-Sure Termination by Guarded Refinement. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Tachis: Higher-Order Separation Logic with Credits for Expected Costs. - Philipp G. Haselwarter; Kwing Hei Li; Markus de Medeiros; Simon Oddershede Gregersen; Alejandro Aguirre 001; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement. - Amin Timany; Simon Oddershede Gregersen; Léo Stefanesco; Jonas Kastberg Hinrichsen; Léon Gondelman; Abel Nieto; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs - Coq Artifact. - Alejandro Aguirre 001; Philipp G. Haselwarter; Markus de Medeiros; Kwing Hei Li; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Zenodo, 2024)

Almost-Sure Termination by Guarded Refinement - Coq Artifact. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Zenodo, 2024)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs - Formalization Artifact. - Philipp G. Haselwarter; Kwing Hei Li; Alejandro Aguirre 001; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Zenodo, 2024)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs. - Philipp G. Haselwarter; Kwing Hei Li; Alejandro Aguirre 001; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2025)

Logical Relations for Formally Verified Authenticated Data Structures. - Simon Oddershede Gregersen; Chaitanya Agarwal; Joseph Tassarotti (CoRR, 2025)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs. - Kwing Hei Li; Alejandro Aguirre 001; Simon Oddershede Gregersen; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (CoRR, 2025)