一句话：提出右线性代数 RLA 与循环证明系统 CRLA，证明其对正则语言及 ω-正则语言的可靠完备性。
右线性（或左线性）文法是刻画正则语言的上下文无关文法子类，也可视为将乘积限制为字母左参数的带最小不动点表达式，从而为正规表达式提供另一种语法。本文研究这一语法所导出的逻辑理论：提出右线性代数（RLA）及其循环证明系统 CRLA，证明 CRLA 对正则语言模型可靠且完备，并通过从循环证明中提取归纳不变式得到 RLA 的完备性。随后为 CRLA 加入最大不动点，得到 vCRLA；由于右线性，它自然由 ω-词语言建模。作者还证明 vCRLA 的守卫片段对 ω-正则语言模型可靠且完备，并借助博弈论技术处理不动点交错。
Right-linear (or left-linear) grammars are a well-known class of context-free grammars computing just the regular languages. They may naturally be written as expressions with least fixed points but with products restricted to letters as left arguments, giving an alternative to the syntax of regular expressions. In this work, we investigate the resulting logical theory of this syntax. Namely, we propose a theory of right-linear algebras (RLA) over this syntax and a cyclic proof system CRLA for reasoning about them. We show that CRLA is sound and complete for the intended model of regular languages. From here we recover the same completeness result for RLA by extracting inductive invariants from cyclic proofs. Finally, we extend CRLA by greatest fixed points, vCRLA, naturally modelled by languages of ω-words thanks to right-linearity. We show a similar soundness and completeness result of (the guarded fragment of) vCRLA for the model of ω-regular languages, this time requiring game theoretic techniques to handle the interleaving of fixed points.