Research
Research Statement
Last updated on 16/11/2022: Research Statement.
Publications
04/2023 |
A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
with
Tobias KappĂ© and
Alexandra Silva.
[To appear 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.
[Appeared 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.
[Appeared 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.
[Appeared 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Ă© and
Dexter Kozen and
Alexandra Silva.
[Appeared 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
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. |