Research Statement

Last updated on 16/11/2022: Research Statement


06/2023 Fractals from Regular Behaviours with Victoria Noquez and Lawrence Moss [Won Best Paper at CALCO 2023!]
(Hover for abstract)
We are interested in connections between the theory of fractal sets obtained as attractors of iterated function systems and process calculi. To this end, we reinterpret Milner's expressions for processes as contraction operators on a complete metric space. When the space is, for example, the plane, the denotations of fixed point terms correspond to familiar fractal sets. We give a sound and complete axiomatization of fractal equivalence, the congruence on terms consisting of pairs that construct identical self-similar sets in all interpretations. We further make connections to labelled Markov chains and to invariant measures. In all of this work, we use important results from process calculi. For example, we use Rabinovich's completeness theorem for trace equivalence in our own completeness theorem. In addition to our results, we also raise many questions related to both fractals and process calculi.
05/2023 Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity with Wojciech Rozowski, Tobias Kappé, Dexter Kozen, and Alexandra Silva [At ICALP 2023]
(Hover for abstract)
We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branching. We give its operational semantics in terms of special class of probabilistic automata. We give a sound and complete Salomaa-style axiomatisation of bisimilarity of ProbGKAT expressions. Finally, we show that bisimilarity of ProbGKAT expressions can be decided in O(n^3log(n)) time via a generic partition refinement algorithm.
04/2023 A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests with Tobias Kappé and Alexandra Silva [At ESOP 2023]
(Hover for abstract)
Guarded Kleene Algebra with Tests (GKAT) is a fragment of Kleene Algebra with Tests (KAT) that was recently introduced to reason efficiently about imperative programs. In contrast to KAT, GKAT does not have an algebraic axiomatization, but relies on an analogue of Salomaa's axiomatization of Kleene Algebra. In this paper, we present an algebraic axiomatization and prove two completeness results for a large fragment of GKAT in the form of skip-free programs.
07/2022 Processes Parametrised by an Algebraic Theory with Wojciech Rozowski, Alexandra Silva, and Jurriaan Rot [At ICALP 2022]
(Hover for abstract)
This paper introduces a family of processa algebras in one parameter: the algebraic theory that presents the branching structure of the processes algebraized. We also cut out nonstandard analogues of regular expressions from a large chunk of these process algebras.
07/2021 How to write a coequation with Fred Dahlqvist [At CALCO 2021]
(Hover for abstract)
This fits into CALCO's new "pearls" submission category. It is part historical survey, part tutorial, and part reference resource. Basically, coequations are very useful, despite their perceived austerity, and we just wanted to make them a little more accessible to the community.
07/2021 On Star Expressions and Coalgebraic Completeness Theorems with Jurriaan Rot and Alexandra Silva [At MFPS 2021]
(Hover for abstract)
This paper is a universal coalgebraic take on the recent significant step made by Clemens Grabmayer and Wan Fokkink towards solving a famous problem posed by Robin Milner. It also contains general accounts of two different approaches to proving coalgebraic completeness theorems found in the literature.
02/2021 Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness with Tobias Kappé, Dexter Kozen, and Alexandra Silva [At ICALP 2021]
(Hover for abstract)
This was a follow-up to the original paper on GKAT, giving a final coalgebra semantics to both the original axiomatisation as well as an axiomatisation for GKAT without the early termination axiom.
12/2019 Concrete Barriers to Quantifier Elimination in Finite-Dimensional C*-algebras with Christopher Eagle [Published in Mathematical Logic Quarterly]
(Hover for abstract)
This was the culmination of what was essentially an undergraduate thesis, funded by a Jamie Cassels Undergraduate Research Award. The primary result is that minimal projectivity and unitary conjugation are definable in the language of C*-algebras, but are inexpressible without quantifiers. Furthermore, adding them to the language is sufficient for quantifier eliination in finite-dimensional C*-algberas (and in fact, only minimal projectivity is needed for the matrix algebras).


08/2022 Presenting with Quantitative Inequational Theories [Presented at BLAST 2022]
(Hover for abstract)
It came to the attention of myself and the coauthors of (S., Rozowski, Silva, Rot, 2022) that a number of process calculi can be obtained by algebraically presenting the branching structure of the transition systems they specify. Labelled transition systems, for example, branch into sets of transitions, terms in the free semilattice generated by the transitions. Interpreting equational theories in the category of sets has undesirable limitations, and we would like to have more examples of presentations in other categories. In this brief article, I discuss monad presentations in the category of partially ordered sets and monotone maps. I focus on quantitative monads, namely free modules over ordered semirings, and give sufficient conditions for one of these to lift a monad on the category of sets.
07/2022 A (Co)algebraic Framework for Ordered Processes
(Hover for abstract)
A recently published paper (Schmid, Rozowski, Silva, and Rot, 2022) offers a (co)algebraic framework for studying processes with algebraic branching structures and recursion operators. The framework captures Milner's algebra of regular behaviours (Milner, 1984) but fails to give an honest account of a closely related calculus of probabilistic processes (Stark and Smolka, 1999). We capture Stark and Smolka's calculus by giving an alternative framework, aimed at studying a family of ordered process calculi with inequationally specified branching structures and recursion operators. We observe that a recent probabilistic extension of guarded Kleene algebra with tests (Rozowski, Kozen, Kappe, Schmid, Silva, 2022) is a fragment of one of our calculi, along with other examples. We also compare the intrinsic order in our process calculi with the notion of similarity in coalgebra.

Talks and Posters

04/2023 Talk: A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
ESOP 2023
in Paris, France
11/2022 Talk: A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
Cornell PLDG Seminar
in Ithaca, New York, USA
11/2022 Talk: A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
Boston University POPV Seminar
in Boston, Massachusetts, USA
11/2022 Talk: Recipes for Process Calculi
Indiana University Logic and Language Seminar
in Bloomington, Indiana, USA
08/2022 Talk: Presenting with Quantitative Inequational Theories
BLAST 2022
in Orange, California, USA
07/2022 Talk: Processes Parametrised by an Algebraic Theory
International Colloquium on Automata, Languages and Programming 2022
in Paris, France
09/2021 Talk: On Star Expressions and Completeness Theorems
Mathematical Foundations of Programming Semantics 2021
07/2021 Talk: Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness
International Colloquium on Automata, Languages, and Programming 2021
04/2021 Talk: Coequations for Guarded Kleene Algebra with Tests
PPLV Seminar
03/2020 Poster: Coalgebras, Covarieties, Coequations
Topics in Category Theory: A Spring School
in Edinburgh, UK


06/2020 Graph Representations for Bunched Implications
(Hover for abstract)
These are notes on some preliminary work I did early in my PhD. I was aiming at a combinatorial proof system for the logic of Bunched Implications, following earlier work of Dominic Hughes, Lutz Strassburger, and Willem Heijltjes (see here).
08/2019 Toposes, Sets, and Cohen Forcing
(Hover for abstract)
This is a writeup of my masters' project, supervised by Stevo Todorcevic at the University of Toronto. It essentially follows the approach to proving the independence of the continuum hypothesis taken in the classic textbook Sheaves in Geometry and Logic by Saunders MacLane and Leke Moerdijk, but as simple as I could manage and with a number of peripheral comments.