6 papers · 1 filter
GKAT with Hoare Hypotheses
Jurriaan Rot, Todd Schmid, Jana Wagemaker
Guarded Kleene Algebra with Tests (GKAT) is a variant of Kleene algebra which allows for reasoning about simple imperative programs, and which features a decision procedure for pro…
The Algebra of Iterative Constructions
Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer +3
Fixed points are a recurring theme in computer science and are often constructed as limits of suitably seeded fixed point iterations. We present the algebra of iterative constructi…
Coalgebraic Path Constraints
Todd Schmid
Axiomatizing covarieties of coalgebras for an endofunctor is less intuitive than axiomatizing varieties of algebras via equations (Dahlqvist and Schmid, 2022). Existing techniques…
Fractals from Regular Behaviours
Todd Schmid, Victoria Noquez, Lawrence S. Moss
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 fo…
A General Completeness Theorem for Skip-free Star Algebras
Tobias Kappé, Todd Schmid
We consider process algebras with branching parametrized by an equational theory T, and show that it is possible to axiomatize bisimilarity under certain conditions on T. Our proof…
A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
Tobias Kappé, Todd Schmid, Alexandra Silva
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…