A Proof Theory of (ω-)Context-Free Languages via Non-Wellfounded Proofs

The authors develop a non-wellfounded proof system, µHKA, that is sound and complete for the equational theory of context-free languages. They then use this result to obtain an alternative proof of completeness for an infinitary axiomatization of the same theory. Finally, they extend the system to handle ω-context-free languages.