Research
Students
Spring 2024 Cohort (St. Mary's College) David Coleman, Undergraduate Research Intern on the Dub Dragon Project
 Andrew Kernycky, Undergraduate Capstone Student on the Dub Dragon Project
 Mary Kyne, Undergraduate Research Intern on the Dub Dragon Project
 Samuel Leitch, Undergraduate Research Intern on the Dub Dragon Project
 Connor Li, Undergraduate Research Intern on the Fractals via Automata Project
Publications
06/2023 
Fractals from Regular Behaviours
with
Victoria Noquez and Lawrence Moss
[Won Best Paper at CALCO 2023!]
(Hover for abstract)
We forge 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 selfsimilar 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.
Update.
We have updated this article a few times now to prepare it for journal submission. Quite a bit has been added, including a bunch of new material about chaos games for regular subfractals and subfractal measures.

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 Salomaastyle 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 Skipfree Guarded Kleene Algebra with Tests
with
Tobias Kappé and
Alexandra Silva
[At ESOP 2023]  but see Note below.
(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 skipfree programs.
Note.
The original edition of this paper contained a gap in the completeness proof (which did not appear in the main text). A complete description of the gap and its correction can be found in Appendix G of the paper on the other side of the link.

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 followup 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 FiniteDimensional 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 finitedimensional C*algberas (and in fact, only minimal projectivity is needed for the matrix algebras). 
Preprints
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
10/2023 
Talk: How to write a coequation: A Tutorial Boston Computation Club in Boston, Massachusetts, USA 
09/2023 
Talk: How to Make Fractals and Melodies with Transition Systems SMC Math Colloquium in Moraga, California, USA 
04/2023 
Talk: A Complete Inference System for Skipfree Guarded Kleene Algebra with Tests ESOP 2023 in Paris, France 
11/2022 
Talk: A Complete Inference System for Skipfree Guarded Kleene Algebra with Tests Cornell PLDG Seminar in Ithaca, New York, USA 
11/2022 
Talk: A Complete Inference System for Skipfree 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 online 
07/2021 
Talk: Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness International Colloquium on Automata, Languages, and Programming 2021 online 
04/2021 
Talk: Coequations for Guarded Kleene Algebra with Tests PPLV Seminar online 
03/2020 
Poster: Coalgebras, Covarieties, Coequations Topics in Category Theory: A Spring School in Edinburgh, UK 
Notes
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. 