Skip to main content

Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness

Seminar by Tobias Kappe (ILLC)

  • Date27 Oct 2021
  • Time 3.00pm-4.00pm
  • Category Seminar

Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness

Abstract

Guarded Kleene Algebra with Tests (GKAT) axiomatizes equivalence between uninterpreted WHILE programs. Like its predecessor Kleene Algebra with Tests (KAT), GKAT comes with a rich algebraic and coalgebraic theory, which gives rise to both completeness and decidability results. Unlike KAT, however, equivalence between GKAT terms can be decided in nearly linear time, for a fixed number of tests.

We study a fragment of GKAT that distinguishes programs that fail immediately from programs that perform some actions before failing, obtained by omitting the so called early termination axiom. Our main result is that this fragment also admits completeness and decidability results, and indeed the same results on the level of GKAT proper follow as a corollary. Our proof method reveals an interesting connection between the semantics of WHILE programs and a something called a "coequation" --- i.e., the categorical dual to an equation.

This is joint work with Todd Schmid, Alexandra Silva, and Dexter Kozen.
tobias.jpeg

Related topics

Explore Royal Holloway

Arrivals Sept 2017 77 1.jpg

Get help paying for your studies at Royal Holloway through a range of scholarships and bursaries.

clubs-societies_REDUCED.jpg

There are lots of exciting ways to get involved at Royal Holloway. Discover new interests and enjoy existing ones.

Accommodation home hero

Heading to university is exciting. Finding the right place to live will get you off to a good start.

Support and wellbeing 2022 teaser.jpg

Whether you need support with your health or practical advice on budgeting or finding part-time work, we can help.

Founders, clock tower, sky, ornate

Discover more about our academic departments and schools.

REF_2021.png

Find out why Royal Holloway is in the top 25% of UK universities for research rated ‘world-leading’ or ‘internationally excellent’.

Immersive Technology

Royal Holloway is a research intensive university and our academics collaborate across disciplines to achieve excellence.

volunteering 10th tenth Anniversary Sculpture - research.jpg

Discover world-class research at Royal Holloway.

First years Emily Wilding Davison Building front view

Discover more about who we are today, and our vision for the future.

RHC PH.100.1.3 Founders south east 1886.w

Royal Holloway began as two pioneering colleges for the education of women in the 19th century, and their spirit lives on today.

Notable alumni Kamaladevi Chattopadhyay

We’ve played a role in thousands of careers, some of them particularly remarkable.

Governance

Find about our decision-making processes and the people who lead and manage Royal Holloway today.