Skip to main content

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

Seminar by Tobias Kappe (ILLC)

  • Date 27 Oct 2021
  • Time 3.00pm-4.00pm
  • Category Seminar

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


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.

Related topics

Explore Royal Holloway

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

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

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

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

Discover more about our academic departments and schools.

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

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

Discover world-class research at Royal Holloway.

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

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

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

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