Pith. sign in

REVIEW 1 cited by

A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2301.11301 v4 pith:NAUISAWQ submitted 2023-01-26 cs.LO cs.PL

Tobias Kappé , Todd Schmid , Alexandra Silva This is my paper · ORCID
classification cs.LOcs.PL
keywords algebrakleeneaxiomatizationgkattestsalgebraicfragmentguarded
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original 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 consisting of skip-free programs.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. On Propositional Program Equivalence (extended abstract)

    cs.PL 2025-07 conditional novelty 2.0 of 10

    The paper reviews GKAT, an algebraic framework with a nearly linear-time decision procedure for propositional program equivalence, and surveys open problems in its axiomatization and expressivity.

Pith tools