Pith. sign in

REVIEW 1 major objections 6 minor 30 references

Algebras for Deterministic Computation Are Inherently Incomplete

T0 review · 1 major / 6 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The deterministic fragment of Kleene Algebra with Tests is not generated by any finite set of regular control flow operations.

desk verdict A genuinely new inexpressivity result for deterministic KAT, proved with an intricate but sound density-transfer argument; worth a serious referee. read the letter →

arxiv 2411.14284 v2 pith:2E4EY7DP submitted 2024-11-21 cs.PL

Balder ten Cate , Tobias Kappé This is my paper · ORCID
classification cs.PL MSC 68Q4568Q70
keywords Kleenealgebrawithtestsdeterministiccontrolflowexpressivenessregularoperationsguardedlanguagesautomatacompositionprogramincompleteness
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Kleene Algebra with Tests (KAT) expresses every non-deterministic finite-state program using just sequencing, nondeterministic choice, and iteration. This paper asks whether some finite set of operations could similarly generate all deterministic finite-state control flow, and answers no: for every finite collection of regular control flow operations (operations definable by deterministic KAT expressions over action and test parameters), there is a deterministic guarded language that no term built from those operations can denote. The witness languages are named $L_k$: they consist of traces whose consecutive atoms are never equal. If correct, this shows that Guarded KAT (GKAT), and every finite extension of it by regular primitives such as repeat-while-changes, remains expressively incomplete, and it settles an open question about finite generation of the deterministic fragment of KAT.

What carries the argument

The central device is a composition operation on deterministic KAT automata, $\mathrm{compose}_{\mathfrak{s}}^{\mathfrak{t}}(A)$, which implements substitution of regular control flow operations at the automaton level and is proved (Propositions 6.5 and 6.12) to match the guarded-language substitution. To handle subprograms that accept immediately, the construction uses shortcut functions $\hat{\delta}$ and $\hat{\iota}$ that skip over accepting subautomata and reject on infinite regression. The incompleteness argument runs on a density measure: the witness languages $L_k$ force any recognizing automaton to be $k$-dense, $k$-dense automata have at least $k$ states, and density cannot be created by composition from smaller automata. The transfer property, Lemma 6.22, says that if a triviality-free composition is $k$-dense then either the outer automaton or one of the substituted subautomata is $k$-dense, and it relies on Lemma 6.14, which says two non-local transitions exiting the same locale execute the same action label.

What would settle it

Exhibit a finite set of deterministic KAT expressions, each defining an automaton with fewer than $k$ states, such that the language $L_k$ (traces whose consecutive atoms always differ) is denoted by some term built from those expressions; Theorem 6.15 forbids exactly this, so testing the $k=3$ case against the standard GKAT operations (each recognized by two-state automata) would settle the base case.

Watch

Extended reading notes

Core claim

The paper proves that the deterministic fragment of Kleene Algebra with Tests (KAT) is not generated by any finite set of regular control flow operations. A regular control flow operation is a composition operator defined by a deterministic KAT expression over formal action and test variables, so it subsumes sequential composition, if-then-else, while-do, and repeat-while-changes. The proof introduces, for each $k$, the deterministic guarded language $L_k$ consisting of traces whose successive atoms are never equal, and shows that any deterministic KAT automaton recognizing $L_k$ must be $k$-dense: it must contain $k$ disjoint clusters of states that are fully connected in a specific pattern, hence at least $k$ states. It then develops a composition operation on deterministic KAT automata corresponding to substitution of regular operations, and proves a transfer property: if a triviality-free composition is $k$-dense, then either the outer automaton or one of the substituted subautomata is $k$-dense. Since any term built from a finite set $O$ only composes automata of bounded size, for sufficiently large $k$ the language $L_k$ cannot be denoted by any such term; Theorem 6.2 and Corollary 6.3 follow. Along the way the paper shows that deciding whether a KAT expression is deterministic is coNP-complete, and polynomial-time for bounded test alphabets, and that an infinite family of 'free automaton' operations does generate the whole deterministic fragment.

Load-bearing premise

The proof stands on the correctness of the automata-composition construction, and within it on the claim that two non-local transitions exiting the same block of states belonging to one substituted subprogram must carry the same action label; if that lemma fails, the density-transfer argument and the incompleteness theorem collapse.

Editorial extensions

If this is right

  • For every finite extension of GKAT by deterministic regular control flow operations, there is a deterministic regular program not expressible in the extension.
  • The deterministic fragment of KAT is not generated by finitely many term-definable operations, resolving an open question about finite generation.
  • There is an infinite, structurally simple family of regular control flow operations (the free automata $O_k$) that does generate all of deterministic KAT.
  • Determinism of a KAT expression is coNP-complete to decide in general, but polynomial-time when the test alphabet is fixed.
  • In contrast, the deterministic fragment of plain Kleene algebra (no tests) is finitely generated by sequential composition plus true and false constants.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural next test is whether the same density-transfer argument shows that deterministic fragments of other Kleene-style algebras with tests, such as Kleene algebra with domain, are also not finitely generated.
  • Because the witness languages $L_k$ are so elementary, the incompleteness likely persists even for richer syntactic bases that include operations with many states, suggesting a hierarchy indexed by the state count of the defining automata.
  • The coNP-completeness result could make deterministic KAT practical for program analysis: verifying that a program is deterministic is feasible for fixed test alphabets, even though no finite basis can generate all such programs.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 6 minor

Summary. This paper studies the expressive power of deterministic control flow operations in the setting of Kleene Algebra with Tests (KAT). The authors define a regular control flow operation as one given by a deterministic KAT expression with action and test parameters, and show that the deterministic fragment of KAT is not generated by any finite set of such operations. The proof introduces a family L_k of deterministic regular guarded languages, develops a composition semantics for deterministic KAT automata (with shortcut functions for immediately accepting subautomata), and proves via a k-density invariant that any automaton built by repeated composition from components with fewer than k states cannot accept L_k. The paper also proves that deciding determinism of a KAT expression is coNP-complete (and polynomial for bounded test alphabets), exhibits an infinite generating set via free automata, and shows that the deterministic fragment of KA without tests is finitely generated.

Significance. If the main theorem is correct, it settles an open question from Bogaerts et al. and generalizes prior inexpressibility results for GKAT. The k-density technique and the composition semantics for deterministic KAT automata are novel and likely to be useful for further expressivity questions in program algebra. The paper is largely self-contained, with clearly stated counterexample languages and mostly detailed proofs; the central construction is parameter-free and the claims are specific and falsifiable. These are substantial contributions to the theory of program algebra and control-flow expressivity.

major comments (1)
  1. [Section 6.1, Proposition 6.12] The proof of Proposition 6.12, which states that the language of the composed automaton equals the substituted guarded language, is reduced to the sentence "Claim 1 can now be proved by induction on w." This claim is the technical core of the composition correctness and is load-bearing for Theorem 6.15 via Lemma 6.22. Please provide the full induction, including the cases where the subautomaton accepts immediately and where the shortcut function rejects by infinite regression, or move the detailed proof to an appendix. As written, the proof is not independently verifiable from the text.
minor comments (6)
  1. [Definition 6.16] In the definition of k-density, the phrase "for all 1≤i,j ≤n" should read "for all 1≤i,j ≤k," since the subscript n is not defined there.
  2. [Lemma 6.21, case (2)] In the third condition of the witness check, the text says "because A is k-dense" when it should refer to the composed automaton; please correct this to avoid confusion.
  3. [Proof of Proposition 4.4] The word "dinstinguish" in the second case of the converse direction is a typo and should be "distinguish."
  4. [Definition 6.1] For n=1, the displayed form of a guarded string in L_k is ambiguous; please state explicitly that the string is just α_{i1} with i1 ≠ 1.
  5. [Section 4.3, Claim 3] The claim that the combined complexity of PDL model checking is polynomial is cited to Fischer and Ladner [1979], but that reference is primarily about satisfiability; the direct bottom-up dynamic-programming argument given in the same paragraph is sufficient and could be presented as the proof.
  6. [Definitions 6.7–6.10] The well-foundedness of the recursive definition of \hat{\delta} is explained in words; a short formal statement that it is the least fixed point of a monotone operator on a finite domain would make the construction easier to check.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: main theorem proved by self-contained density-transfer argument; only self-citation is motivational.

full rationale

The main theorem (Theorem 6.2, Corollary 6.3) is derived from first principles in Section 6. The counterexample languages L_k (Definition 6.1) are fresh, parameter-free constructions. The automata-composition semantics (Definitions 6.7–6.10) is introduced and proved correct by Proposition 6.5 via Propositions 6.6 and 6.12; the proof of Proposition 6.12 is compressed but is an induction on w, not an appeal to the target theorem. The density-transfer chain (Lemmas 6.17–6.22) is self-contained: Lemma 6.17 derives k-density of any automaton for L_k from the definition of L_k, Lemma 6.18 is a counting argument from determinism, and Lemmas 6.19–6.22 transfer density through composition using only the local/non-local transition analysis and Lemma 6.14. No parameter is fitted to the target result, and no 'prediction' is renamed as an input. The only citation to co-authored prior work, Theorem 4.9 (Schmid et al. 2021, Lemma D.2), supports the motivational Theorem 2.4 and is not used in the proof of Theorem 6.2; it is therefore not load-bearing. The compressed proof of Proposition 6.12 is a presentation risk, not a circularity.

Assumptions & free parameters 0 free parameters · 8 assumptions · 2 invented entities

The central claim rests on standard KAT bedrock theorems imported from the literature (Kozen-Smith correspondence, Kleene theorem for KAT), two textbook fixed-point arguments, and one cited lemma (Schmid et al. 2021, Lemma D.2) used only for the motivating example. No free parameters are fitted, no ad hoc constants are introduced; the existential k in Theorem 6.2 is a proof variable, not a fitted value. The new mathematical objects (L_k, k-density, free automata A_k) are explicit constructions with checkable definitions, so they are not 'graviton-style' invented entities.

assumptions (8)
  • standard math Dependent functional extensionality for the dependently typed semantics (Section 2.3, footnote 1: 'We assume dependent functional extensionality').
    Standard metatheoretic assumption in type-theoretic presentations; explicitly flagged by the authors; does not enter the finite-state automata arguments of Sections 5-7.
  • standard math Kleene's fixed point theorem (Scott-continuity on the DCPO of partial functions) defines the while-loop semantics and the mutually recursive u, v for the program F (Remark 2.1 and Definition 2.3).
    Justifies the least-fixed-point semantics of loops; textbook domain theory, used to set up the motivating examples only.
  • domain assumption Relational and guarded-string semantics of KAT coincide (Proposition 3.6, cited to Kozen and Smith 1996); all results transfer freely between R[[-]] and L(-).
    Imported as a cited theorem with a proof sketch given in the paper; it is the bridge that lets the main inexpressivity result be stated in either semantics.
  • domain assumption Kleene theorem for KAT: KAT expressions and KAT automata define the same guarded languages (Proposition 3.11, cited to Kozen 2003).
    Basis for the automata-theoretic formulation of regular control flow operations and for the coNP-completeness argument in Theorem 4.13.
  • domain assumption Theorem 4.9 (Schmid et al. 2021, Lemma D.2): no GKAT expression has the language tp(tptp)*(t+tpt).
    Used in the proof of the illustrative Theorem 2.4 only; the main Theorem 6.2 is proved independently in Section 6 without importing this lemma.
  • domain assumption GKAT and KAT expressions are closed under Brzozowski derivatives (Chen and Pucella 2004; Smolka et al. 2020), invoked in the proof of Theorem 2.4.
    Powers the extraction of the subexpression tp(tptp)*(t+tpt) in that proof; the extraction step itself is only sketched in the text as something that 'should then be possible'.
  • domain assumption PDL model checking has polynomial combined complexity (Fischer and Ladner 1979), used in the coNP upper bound of Theorem 4.13.
    Shortcut for deciding membership of a guarded string in L(e); standard cited result, not proved in the paper.
  • standard math Myhill-Nerode theorem for regular languages, used in Proposition 4.12 to bound the derivative set R(L).
    Routine automata theory; ensures the Brzozowski-derived deterministic automaton for a deterministic regular language is finite.
invented entities (2)
  • Counterexample guarded languages L_k (Definition 6.1). independent evidence
    purpose: Witness that for any finite operator set O, some deterministic regular language escapes generation by O.
    Fully explicit definition plus proved properties (determinism, Lemma 6.17 forcing k-density on any recognizer); an independent verifier can directly check membership and recognizer size.
  • The k-density predicate on deterministic KAT automata (Definition 6.16). independent evidence
    purpose: Composition-transferable invariant that yields the lower bound on recognizer states and the non-generation theorem.
    Defined purely syntactically on automata states; Lemmas 6.17-6.22 give checkable transfer properties. Both entities are constructed proof devices, not unsupported postulates.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Algebras for Deterministic Computation Are Inherently Incomplete." pith.science (2026). https://pith.science/paper/2E4EY7DP

@misc{pith2026241114284,
  author       = {Pith},
  title        = {Pith review of: Algebras for Deterministic Computation Are Inherently Incomplete},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2E4EY7DP}},
  note         = {Machine review of arXiv:2411.14284}
}
read the original abstract

Kleene Algebra with Tests (KAT) provides an elegant algebraic framework for describing non-deterministic finite-state computations. Using a small finite set of non-deterministic programming constructs (sequencing, non-deterministic choice, and iteration) it is able to express all non-deterministic finite state control flow over a finite set of primitives. It is natural to ask whether there exists a similar finite set of constructs that can capture all deterministic computation. We show that this is not the case. More precisely, the deterministic fragment of KAT is not generated by any finite set of regular control flow operations. This generalizes earlier results about the expressivity of the traditional control flow operations, i.e., sequential composition, if-then-else and while.

Figures

Figures reproduced from arXiv: 2411.14284 by the authors.

Figure 1
Figure 1. Visualization of a KAT automaton on 𝑄 = {𝑞1} (left), with transitions 𝛿 and initialization 𝜄 (right). Definition 3.8. A KAT automaton is a triple 𝐴 = (𝑄, 𝛿, 𝜄), where 𝑄 is a finite set of states, 𝛿 : 𝑄 × At → 2 {accept}+Σ×𝑄 is the transition function and 𝜄 : At → 2 {accept}+Σ×𝑄 is the initialization function. The guarded language accepted in 𝐴 by 𝛾 : At → 2 {accept}+Σ×𝑄 , denoted 𝐿𝐴 (𝛾), is defined as the smallest s… view at source ↗
Figure 2
Figure 2. KAT automaton modeling the “repeat 𝑝 until 𝑡 changes” program 𝐹 . 3.5 Programmable Control Flow We started this section with the goal of formalizing what it meant for control flow to be pro￾grammable. To that end, we considered KAT as a generalization of GKAT that includes non￾determinism. We have seen how the relational semantics of KAT extends the partial function semantics of GKAT, and how the former can be relat… view at source ↗
Figure 3
Figure 3. At the top, a map 𝔰 from Σ2 = {𝑝1, 𝑝2} to automata over 𝑇 = {𝑡, 𝑡′ , 𝑡′′} and Σ = {𝑝, 𝑝′ , 𝑝′′}. On the bottom left, an automaton 𝐴 = (𝑄, 𝛿, 𝜄) over 𝑇0 = ∅ and Σ2, representing the operator 𝑝1 · 𝑝2. On the bottom right, the automaton (𝑄, ˆ𝛿, 𝜄ˆ) obtained from 𝐴, with ˆ𝛿 and 𝜄ˆ derived from 𝛿 and 𝜄 per Definitions 6.7 and 6.8. This definition is recursive, but the last case handles infinite regression, which makes ˆ𝛿… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: On the left, the automaton (𝑄, ˆ𝛿, 𝜄ˆ) from [PITH_FULL_IMAGE:figures/full_fig_p019_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

30 extracted references · 14 canonical work pages

  1. [14]

    KAT + B!

    “KAT + B!” In: CSL-LICS, 44:1–44:10. doi: https://doi.org/10.1145/2603088.2603095. Tobias Kappé, Todd Schmid, and Alexandra Silva

    work page arXiv

  2. [15]

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

    “A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests. ” In:ESOP, 309–336. doi: https://doi.org/10.1007/978-3-031-30044-8_12. Stephen C. Kleene

    doi:10.1007/978-3-031-30044-8_12

  3. [21]

    Kleene Algebra with Tests: Completeness and Decidability

    “Kleene Algebra with Tests: Completeness and Decidability. ” In:Proc. Computer Science Logic (CSL), 244–259. doi: https://doi.org/10.1007/3-540-63172-0_43. Dexter Kozen and Wei-Lung Dustin Tseng

    doi:10.1007/3-540-63172-0_43

  4. [22]

    The Böhm-Jacopini Theorem Is False, Propositionally

    “The Böhm-Jacopini Theorem Is False, Propositionally. ” In:MPC, 177–192. doi: https://doi.org/10.1007/978-3-540-70594-9_11. Robin Milner

    doi:10.1007/978-3-540-70594-9_11

  5. [24]

    On the interpretation of recursive program schemes . Tech. rep. doi: https://doi.org/10.22028/D291-26058. W. Wesley Peterson, Tadao Kasami, and Nobuki Tokura

    work page doi:10.22028/d291-26058

  6. [25]

    On the Capabilities of While, Repeat, and Exit Statements

    “On the Capabilities of While, Repeat, and Exit Statements. ” Commun. ACM, 16, 8, 503–512. doi: https://doi.org/10.1145/355609.362337. Damien Pous

    arXiv

  7. [28]

    Kleene Algebra with Dynamic Tests: Completeness and Complexity . (2023). doi: https://doi.org/10.48550 /ARXIV.2311.06937. Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva

    arXiv doi:10.48550/arxiv.2311.06937 2023

  8. [30]

    Publication date: January 2025

    2025

Show all 30 references
  1. [1964]

    Derivatives of Regular Expressions

    “Derivatives of Regular Expressions. ”J. ACM, 11, 4, 481–494. doi: https://doi.org/10.1145/32123 9.321249. Hugues Cassé, Louis Féraud, Christine Rochange, and Pascal Sainrat

    doi

  2. [1966]

    Flow diagrams, turing machines and languages with only two formation rules

    “Flow diagrams, turing machines and languages with only two formation rules. ” Commun. ACM, 9, 5, 366–371. doi: https://doi.org/10.1145/355592.365646. Janusz A. Brzozowski

  3. [1971]

    Notes on Avoiding

    “Notes on Avoiding "go to" Statements. ”Inf. Process. Lett. , 1, 1, 23–31. doi: https://doi.org/10.1016/0020-0190(71)90018-4. S. Rao Kosaraju

    doi

  4. [1973]

    Program Schemes, Recursion Schemes, and Formal Languages

    “Program Schemes, Recursion Schemes, and Formal Languages. ”J. Comput. Syst. Sci., 7, 2, 119–160. doi: https://doi.org/10.1016/S0022-0000(73)80040-6. Clemens Grabmayer

    doi

  5. [1974]

    Analysis of Structured Programs

    “Analysis of Structured Programs. ”J. Comput. Syst. Sci. , 9, 3, 232–255. doi: https://doi.org/10.1016/S00 22-0000(74)80043-7. Dexter Kozen

    doi

  6. [1979]

    Propositional Dynamic Logic of Regular Programs

    “Propositional Dynamic Logic of Regular Programs. ”J. Comput. Syst. Sci. , 18, 2, 194–211. doi: https://doi.org/10.1016/0022-0000(79)90046-1. Stephen J. Garland and David C. Luckham

    doi

  7. [1984]

    A Complete Inference System for a Class of Regular Behaviours

    “A Complete Inference System for a Class of Regular Behaviours. ”J. Comput. Syst. Sci. , 28, 3, 439–466. doi: https://doi.org/10.1016/0022-0000(84)90023-0. Maurice Nivat

    doi

  8. [1994]

    Taming Control Flow: A Structured Approach to Eliminating Goto Statements

    “Taming Control Flow: A Structured Approach to Eliminating Goto Statements. ” In: ICCL. IEEE Computer Society, 229–240. doi: https://doi.org/10.1109/ICCL.1994.288377. Michael J. Fischer and Richard E. Ladner

    1994

  9. [1996]

    Partial Derivatives of Regular Expressions and Finite Automaton Constructions

    “Partial Derivatives of Regular Expressions and Finite Automaton Constructions. ” Theor. Comput. Sci., 155, 2, 291–319. doi: https://doi.org/10.1016/0304-3975(95)00182-4. Edward A. Ashcroft and Zohar Manna

    doi

  10. [1997]

    Kleene Algebra with Tests

    “Kleene Algebra with Tests. ”ACM Trans. Program. Lang. Syst., 19, 3, 427–443. doi: https://doi.org/10.114 5/256167.256195. Proc. ACM Program. Lang., Vol. 9, No. POPL, Article

  11. [2000]

    Certification of Compiler Optimizations Using Kleene Algebra with Tests

    “Certification of Compiler Optimizations Using Kleene Algebra with Tests. ” In: CL, 568–582. doi: https://doi.org/10.1007/3-540-44957-4_38. Dexter Kozen and Frederick Smith

    doi

  12. [2001]

    Kleene Algebra with Tests and Program Schematology . Tech. rep. TR2001-1844. Cornell University, (July 2001). Valentin M. Antimirov

    2001

  13. [2004]

    A coalgebraic approach to Kleene algebra with tests

    “A coalgebraic approach to Kleene algebra with tests. ”Theor. Comput. Sci., 327, 1-2, 23–44. doi: https://doi.org/10.1016/j.tcs.2004.07.020. Ernie Cohen, Dexter Kozen, and Frederick Smith. July 1996.The Complexity of Kleene Algebra with Tests. Tech. rep. TR96-1598. (July 1996)...

    2004 doi

  14. [2006]

    Kleene algebra with domain

    “Kleene algebra with domain. ”ACM Trans. Comput. Log., 7, 4, 798–833. doi: https://doi.org/10.1145/1183278.1183285. Ana M. Erosa and Laurie J. Hendren

  15. [2008]

    Nonlocal Flow of Control and Kleene Algebra with Tests

    “Nonlocal Flow of Control and Kleene Algebra with Tests. ” In:LICS, 105–117. doi: https://doi.org/10.11 09/LICS.2008.32. Dexter Kozen

    2008

  16. [2014]

    NetKAT: semantic foundations for networks

    “NetKAT: semantic foundations for networks. ” In:POPL, 113–126. doi: https://doi.org/10.1145/2535838.2535862. Allegra Angus and Dexter Kozen. July

  17. [2015]

    Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests

    “Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests. ” In:POPL, 357–368. doi: https://doi.org/10.1145/2676726.2677007. Todd Schmid, Tobias Kappé, Dexter Kozen, and Alexandra Silva

  18. [2020]

    A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilar- ity

    “A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilar- ity. ” In:LICS. ACM, 465–478. doi: https://doi.org/10.1145/3373718.3394744. Niels Bjørn Bugge Grathwohl, Dexter Kozen, and Konstantinos Mamouras

  19. [2021]

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

    “Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness. ” In:ICALP. Vol. 198, 142:1–142:14. doi: https://doi.org/10.4230/LIPICS.ICALP.2021.142. Igor Sedlár

    2021 doi

  20. [2022]

    Milner’s Proof System for Regular Expressions Modulo Bisimilarity is Complete

    “Milner’s Proof System for Regular Expressions Modulo Bisimilarity is Complete. ” In:LICS. ACM, 34:1–34:13. doi: https://doi.org/10.1145/3531130.3532430. Clemens Grabmayer and Wan J. Fokkink

  21. [2023]

    Preservation theorems for Tarski’s relation algebra. (2023). doi: https://doi.org/10.48550/ARXIV.2305.04656. Corrado Böhm and Giuseppe Jacopini

    2023 doi arXiv

  22. [2024]

    CF-GKAT: Efficient Validation of Control-Flow Transformations

    “CF-GKAT: Efficient Validation of Control-Flow Transformations. ” In:POPL, 21:1–21:27. doi: https://doi.org/10.1145/3704857. Received 2024-07-09; accepted 2024-11-07 Proc. ACM Program. Lang., Vol. 9, No. POPL, Article

    2024 doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.