# Dan Frumin (home page)

## About

I am a postdoc researcher in Jorge Perez’s group Fundamental Computing, working on session types and processes-as-proofs interpretations.

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.

My research is focused around formal verification, program logics, semantics, and type theory, especially with applications to concurrency.

### Contact information

- Email: dan `at` groupoid.moe
- Office: Bernoulliborg (5161) 0411

## Writings

### Preprints / drafts

Semantic cut elimination for the logic of Bunched Implications, formalized in Coq

*Draft, 2021*Coq formalization

We demonstrate how to prove cut elimination for the BI sequent calculus in a semantic way, by extending Okada’s phase-semantic proof of cut elimination for ILL. We show that this approach scales to extensions of BI with a large class of structural rules, and an S4-like modality. We formalize the proof in the Coq assistant.

Mechanized Verification of a Fine-Grained Concurrent Queue from Facebook’s Folly Library

with Simon Friis Vindum and Lars Birkedal

*Draft, 2021*We prove linearizability of a concurrent multi-producer/multi-consumer queue from the Folly library.

Bicategories in Univalent Foundations

with Benedikt Ahrens, Niels van der Weide, Marco Maggesi, and Niccolò Veltri

*In submission; extended an overhauled version of the FSCD 2019 paper*We formulate and study weak 2-categories in the context of UniMath. We argue that the “correct” notion in this setting is a

*univalent bicategory*, and we show that “strictification” embeds a locally univalent bicategory into a univalent one. To aid construction of univalent bicategories we introduced*displayed bicategories*, which are sort of “bicategories over a base bicategory” kind of structures. These displayed bicategories allows us to construct complex structures in several layers.

### Publications

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*How can we formally prove refinements between concurrent imperative programs? We introduce a relational separation logic ReLoC for proving and combing (typed) program refinements. We can prove refinements by symbolic execution and formulate things like conditional refinements. ReLoC allows us to prove many interesting refinements in a modular way.

Compositional Non-Interference for Fine-Grained Concurrent Programs

with Robbert Krebbers and Lars Birkedal

*Security & Privacy 2021*Coq sources, Recorded talkGiven a program that operates on some secret data, how do we ensure that the program does not leak this data to an external attacker? In this paper we devise a separation logic SeLoC for proving a strong form of non-interference for concurrent imperative programs. With SeLoC we can analyze fine-grained concurrent programs against flexible (value-dependent) security policies. We use SeLoC as a base to build a simple type system and prove its soundness.

- Bicategories in Univalent Foundations

with Benedikt Ahrens, Niels van der Weide, and Marco Maggesi

*FSCD 2019; superseded by arXiv:1903.01152* Semi-automated reasoning about non-determinism in C expressions

with Léon Gondelman and Robbert Krebbers

*ESOP 2019*Accompanying web page, Coq formalizationIn a C expression

`e0 = e1 + e2`

, the execution of sub-expressions`e2`

,`e1`

, and`e0`

can be interleaved freely. To make sure that all such interleavings are correct, C includes what we call “sequence point violations” – if`e2`

and`e0`

or`e1`

write to the same variable, then the whole expression has*undefined behavior*. We describe a semantics of a C-like language λMC which formalizes this sequence point condition, using a concurrent ML-like meta-language. The semantics is given using a particular monad. From a separation logic for the meta-language we derive a separation logic for the monadic language, allowing us to use separation logic to reason about the semantics that we have defined. Furthermore, we program and verify a verification condition generator, that allows us to automate many steps in the verification of λMC programs.- ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency

with Robbert Krebbers and Lars Birkedal

*LICS 2018; superseded by arXiv:2006.13635* 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

In constructive mathematics there are several notions of “finiteness” for sets. In this paper we study Kuratowski finiteness, specifically in the setting of HoTT. We define a finite power“set” functor as a higher inductive type, which gives rise to notions of a “Kuratowski-finite type” and a “Kuratowski-finite subobject”. For h-sets, we compare those notions with the more standard ones from constructive mathematics.

A homotopy-theoretic model of function extensionality in the effective topos

with Benno van den Berg

*Mathematical Structures in Computer Science, 2018*We give a model of type theory with an interval type in the effective topos (Eff). This model is given from a particular homotopical structure on Eff. This is not quite a model category on Eff, but it is if we take the full subcategory Eff

_{f}on fibrant objects.Actually, this construction of a model category on the subcategory of fibrant objects can be done for any elementary topos, which we show in the first part of the paper. This is a generalization of a Cisinski model structure for a Grothendieck topos.

### Other / 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/proofs (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

- Program Correctness, 2021.

Lecture slides (.pdf), Why3, Why3 tutorial

### Old teaching

- 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

- GroLog seminar
- Bernoulli Institute Colloquia Computer Science
- Categories and Types Seminar (CATS) (UvA)
- Software Science Seminar (Radboud)
- Logseminar (Aarhus)
- Online Worldwide Seminar on Logic and Semantics (Worldwide-ish)