Publications
Writings/publications
- Around Classical and Intuitionistic Linear Processes
CONCUR, 2024, with Juan C. Jaramillo and Jorge A. Pérez
- Interval Domain in Homotopy Type Theory
with Niels van der Weide
Logics and Type Systems in Theory and Practice, 2024, dedicated to Herman Geuvers, on the occasion of his 60th birthday
- Modular Denotational Semantics for Effects with Guarded Interaction Trees
with Amin Timany and Lars Birkedal
POPL, 2024, Distinguished Paper Award, Coq formalization
- A Minimal Formulation of Session Types
in submission, 2023, with Alen Arslanagić and Jorge A. Pérez
- Semantic Cut Elimination for the Logic of Bunched Implications and Structural Extensions, Formalized in Coq
in submission, 2023, Coq formalization, slides the GroLog talk.
This is an extended version of the CPP 2022 paper, including more
details on the formalization and a new section/formalization on
analytic completion of structural rules.
- A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
with Emanuele D’Osualdo, Bas van den Heuvel, and Jorge A. Pérez
OOPSLA 2022
- Semantic cut elimination for the logic of Bunched Implications, formalized in Coq
CPP 2022, Distinguished Paper Award, Coq formalization, slides, video
- Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library
with Simon Friis Vindum and Lars Birkedal
CPP 2022, Coq formalization as part of ReLoC
- Bicategories in Univalent Foundations
with Benedikt Ahrens, Niels van der Weide, Marco Maggesi, and Niccolò Veltri
Mathematical Structures in Computer Science, 2020 (Special Issue on Homotopy Type Theory); extended an overhauled version of the FSCD 2019 paper
- ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
with Robbert Krebbers and Lars Birkedal
LMCS, 2021. Supersedes the LICS’18 paper
- Compositional Non-Interference for Fine-Grained Concurrent Programs
with Robbert Krebbers and Lars Birkedal
Security & Privacy 2021 Coq sources, Recorded talk
- Bicategories in Univalent Foundations
with Benedikt Ahrens, Niels van der Weide, and Marco Maggesi
FSCD 2019. This is superseded by the journal version.
- Semi-automated reasoning about non-determinism in C expressions
with Léon Gondelman and Robbert Krebbers
ESOP 2019. Accompanying web page, Coq formalization
- ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
with Robbert Krebbers and Lars Birkedal
LICS 2018. This is superseded by the journal version.
- Finite Sets in Homotopy Type Theory
with Herman Geuvers, Léon Gondelman, and Niels van der Weide
CPP 2018. Web page with the artifact and the slides
- A homotopy-theoretic model of function extensionality in the effective topos
with Benno van den Berg
Mathematical Structures in Computer Science, 2018
