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

January 26, 2023 · The Ethereal · 🏛 European Symposium on Programming

🔮 THE ETHEREAL: The Ethereal
Pure theory — exists on a plane beyond code

"No code URL or promise found in abstract"

Evidence collected by the PWNC Scanner

Authors Tobias Kappé, Todd Schmid, Alexandra Silva arXiv ID 2301.11301 Category cs.LO: Logic in CS Cross-listed cs.PL Citations 8 Venue European Symposium on Programming Last Checked 5 months ago
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.
Community shame:
Not yet rated
📄 View on arXiv 🌐 View on ar5iv 📑 PDF 🎉 Report Code Found
Community Contributions

Found the code? Know the venue? Think something is wrong? Let us know!

📜 Similar Papers

In the same crypt — Logic in CS