Research

(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 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.

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.

(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.

(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.

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.

(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.

(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.

(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.

(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.

(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).

(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.

(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.

(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).

(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.