# Dan (Daniel) Frumin

## About me

I am a logician and a computer scientist in Fundamental Computing group at the University of Groningen. I am interested in concurrent programs and reasoning about their behavior. My research interest include

- semantics of programming languages;
- program verification and concurrent separation logics;
- substructural logics and their proof theory;
- type theory and type systems;
- formal proofs and proof assistants (especially Univalent Foundations).

### Brief bio

I finished my PhD under the supervision of Herman Geuvers, Freek Wiedijk, and Robbert Krebbers at Radboud University Nijmegen. My thesis is available online, together with the associated Coq mechanizations. After my PhD, I have been a postdoc with Lars Birkedal at the Logic and Semantics group, and a postdoc with Jorge Pérez at the Fundamental Computing group.

### Student projects

If you are a student and you are interested in doing a project (be it a short project or a thesis) related to one of the topics mentioned above, then please do not hesitate to contact me.

See here for a list of previous student projects offered from our group.

### Contact information

- Email: d.frumin `at’ rug.nl
- Office: Bernoulliborg (5161)0414

## 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*

### 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)
- 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) - Notes on the Abadi-Plotkin logic (2016, updated 2019)
- Introduction to delimited continuations (sometime 2017/updated 2018)
- Frobenius property of a weak factorisation system (2016ish)
- Diagonal argument(s) and Lawvere’s fixed point theorem (2015ish)

## Teaching

### Current teaching

At the University of Groningen:

- Languages and Machines (2024)
- Intro to Logic (2023), Models and Semantics of Computation (2023)

All the information is available on the BrightSpace. See also the Education section on the FC webpage.

#### Old teaching links

- 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 (Groningen)
- Bernoulli Institute Colloquia Computer Science (Groningen)
- BI’s Maths Event Calendar (Groningen)
- NetTCS: Network, Types, Coalgebras, Semantics (NL)
- Dutch Categories And Types seminar (NL)
- Logseminar (Aarhus)
- Software Science Seminar (Radboud)
- Online Worldwide Seminar on Logic and Semantics (Worldwide-ish)

## Misc

- Some misc code/formalisations I wrote
- a very small hott-coq quickref | gnomes wearing hats | hamster.html
- The “What Is…?” column from the Notices of the AMS archive
- Weather | buienradar | Central station
- The name of this website is a nod to the ’96 paper of Hofmann and Streicher, and the amazing webpage of Ronald Brown and his book on topology