← 研踪 PaperTrailarXiv:2611.14201 · v1
CFGKAT: A Complete Calculus for Non-Local Control Flow
首次提交 2026-11-10 23:22
版本更新 2026-11-10 23:22
雷达观测 2026-11-11 13:08
摘要
CFGKAT is an extension of guarded Kleene Algebra with Tests (GKAT) that adds non-local control flow (e.g., break, goto) while maintaining an efficient decision procedure. An axiomatization of equivalence for CFGKAT presents unique barriers created by the presence of non-local control flow and contextual semantics of goto which compromises compositional reasoning. In this paper, we overcome these barriers and present a sound and complete axiomatization of program equivalence in CFGKAT. We verify the loop case of the Erosa-Hendren goto elimination algorithm, a difficult syntactic metatheorem which requires reasoning about fixpoints, control-flow contexts, and mutable state. We mechanize the metatheory and case study in Rocq.
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v1 · 2026-11-10 23:22 · 最新观测版本
CFGKAT: A Complete Calculus for Non-Local Control Flow
CFGKAT is an extension of guarded Kleene Algebra with Tests (GKAT) that adds non-local control flow (e.g., break, goto) while maintaining an efficient decision procedure. An axiomatization of equivalence for CFGKAT presents unique barriers created by the presence of non-local control flow and contextual semantics of goto which compromises compositional reasoning. In this paper, we overcome these barriers and present a sound and complete axiomatization of program equivalence in CFGKAT. We verify the loop case of the Erosa-Hendren goto elimination algorithm, a difficult syntactic metatheorem which requires reasoning about fixpoints, control-flow contexts, and mutable state. We mechanize the metatheory and case study in Rocq.
查看此版本解读 →查看此版本原文 ↗