Dan Frumin (home page)
About
I am an assistant professor (UD) in the Fundamental Computing group at the University of Groningen.
My research is focused around formal verification, program logics, semantics, and type theory, especially with applications to concurrency.
If you would like to do a student project on any of those topics, please get into contact with me.
Before that I was a postdoc with Lars Birkedal at the Logic and Semantics group, and a postdoc with Jorge Perez at the Fundamental Computing group.
Previously, I did my PhD under the supervision of Herman Geuvers, Freek Wiedijk, and Robbert Krebbers. My thesis is available online, together with the associated Coq mechanizations.
I have contributed to the Coq formalizations of UniMath and Iris.
Contact information
- Email: dan `at’ groupoid.moe
- Office: Bernoulliborg (5161) 0411
Writings/publications
Preprints
- Modular Denotational Semantics for Effects with Guarded Interaction Trees
in submission, 2023, with Amin Timany and Lars Birkedal Semantic Cut Elimination for the Logic of Bunched Implications and Structural Extensions, Formalized in Coq
in submission, 2023, Coq formalization, slides the GroLog talkThis 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 Minimal Formulation of Session Types
in submission, 2023, with Alen Arslanagić and Jorge A. Pérez
Published
- A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
OOPSLA 2022, with Emanuele D’Osualdo, Bas van den Heuvel, and Jorge A. Pérez - Semantic cut elimination for the logic of Bunched Implications, formalized in Coq
CPP 2022, distinguished paper, 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 2019This 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 2018This 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
Unpublished
- Concurrent Separation Logics for Safety, Refinement, and Security (PhD Thesis; under the supervision of Robbert Krebbers, Herman Geuvers, and Freek Wiedijk, 2021)
- Weak Factorisation Systems in the Effective Topos (MSc Thesis; under the supervision of Benno van den Berg, 2016)
- Logic and homotopy in the category of assemblies (Study report; under the supervision of Jaap van Oosten, 2016)
- Categorical models of type theory (Essay/study report; written with Auke Booij, 2015)
- Presheaf models for concurrency (Study report; under the supervision of Giovanni Ciná, 2015)
- Notes (pdf)
- Notes on the Abadi-Plotkin logic (2016, updated 2019)
- Frobenius property of a weak factorisation system (2016ish)
- Diagonal argument(s) and Lawvere’s fixed point theorem (2015ish)
- Blog posts (html)
- Leibniz equality for truncated types in HoTT (or, defining Leibniz equality with truncation in mind, jan 2021)
- Counterexamples of algebraic theories (how to show that certain categories are not algebraic? jan 2021)
- Introduction to delimited continuations (sometime 2017/updated 2018)
Teaching
- Intro to Logic (2023), Models and Semantics of Computation (2023)
Old teaching
- Program Correctness, 2021, 2022
Why3, Why3 tutorial - Type Theory and Coq, 2019/2020
In the final part of the course we look at MetaCoq/TemplateCoq. See also a recent overview of MetaCoq. - Co-TA (with Niels) for Type Theory and Coq, 2018/2019.
The topic for the last part of the course is guarded type theory. - TA for Type Theory and Coq, 2017/2018.
In the final part of the course we will be looking at continuation passing style and CPS transformations. - TA for Type Theory and Coq, 2016/2017.
In the final part of the course we looked into logical relations. Extra materials: Contextual equivalence proof for logical relations, example proofs in the Abadi-Plotkin logic. UPDATE: there is now an even more comprehensive introduction to logical relations by Lau Skorstengaard: arXiv:1907.11133. - TA for Berekenbaarheid (Computability), 2016, 2018.
Extra materials: some exercises on reductions and Rice’s theorem.
Seminars and meetings
- Stroopt seminar (Groningen)
- GroLog seminar
- Bernoulli Institute Colloquia Computer Science
- Categories and Types Seminar (CATS) (UvA)
- Software Science Seminar (Radboud)
- Dutch Categories And Types seminar
- Logseminar (Aarhus)
- Online Worldwide Seminar on Logic and Semantics (Worldwide-ish)
