Dan Frumin (home page)

Semantic Cut Elimination for the Logic of Bunched Implications and Structural Extensions, Formalized in Coq
in submission, 2022, 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 Minimal Formulation of Session Types
in submission, 2023, with Alen Arslanagić and Jorge A. Pérez

We study a minimal formulation of session types without sequencing. We show how to forgoing sequencing in types, and only with sequencing on the level of processes, we can recover the usual theory of session types. More specifically, we show an encoding of regular session types into minimal session types, grounded in Parrow’s decomposition of a pi-calculus process into a collection of trios. We show that the correctness of the decomposition using a form of a session-typed bisimulation.

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

We study propositions-as-sessions/processes-as-proofs interpretation of the BI sequent calculus. To achieve this interpretation we develop a new π-calculus based process algebra and a type system based on BI types. The resulting type system satisfies deadlock-freedom and is weakly normalizing. We also study it’s observational equivalence theory using relatively simple denotational semantics.

Semantic cut elimination for the logic of Bunched Implications, formalized in Coq
CPP 2022, distinguished paper, Coq formalization, slides, video

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 Meta’s Folly Library
with Simon Friis Vindum and Lars Birkedal
CPP 2022, Coq formalization as part of ReLoC

We prove linearizability of a concurrent multi-producer/multi-consumer queue from the Facebook’s Folly library, which is designed to be highly optimized and for use in production, including in Facebook’s Distributed Data Store for the Social Graph.

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

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.

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 talk

Given 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

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

In 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

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

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.

• 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)

• 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)