Dan Frumin (home page)
About
I am a postdoc researcher in the Logic and Semantics group working with Lars Birkedal on modeling and reasoning about effectful computations.
Previously, I was a postdoc researcher in Jorge Perez’s group Fundamental Computing, working on session types and processes-as-proofs interpretations. 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: Turing (building 5341)
Writings
Preprints
Semantic Cut Elimination for the Logic of Bunched Implications and Structural Extensions, Formalized in Coq
in submission, 2022, 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
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.
Publications
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 paperWe 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 paperHow 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 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 formalizationIn a C expression
e0 = e1 + e2
, the execution of sub-expressionse2
,e1
, ande0
can be interleaved freely. To make sure that all such interleavings are correct, C includes what we call “sequence point violations” – ife2
ande0
ore1
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 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 slidesIn 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, 2018We 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 Efff 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.
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
- Program Correctness, 2021, 2022
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)
- Dutch Categories And Types seminar
- Logseminar (Aarhus)
- Online Worldwide Seminar on Logic and Semantics (Worldwide-ish)