Research
Research Statement
Last updated on 16/11/2022: Research Statement
Publications
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). |
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
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 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. |