Description Operator Precedence Languages (OPL), introduced by Floyd and revived in recent years by the research group, are a subclass of deterministic context-free languages with remarkable algebraic and logic properties: closure under Boolean operations, characterization in terms of automata and monadic second-order logic, and a local parsability property enabling parallel parsing. Their theory has been developed and proved in the traditional literature but has never been formalized in a proof assistant.
This project aims to formalize the core of the OPL theory in the Lean4 language: the fundamental definitions (precedence alphabet and matrix, chains, operator precedence automata and the language they recognize) and the mechanical proof of some of their properties, starting from closure under intersection via the product automaton construction. The formalization serves both as an independent, machine-checked verification of known results and as a reusable basis for extending to further properties.
Technologies
Lean (https://lean-lang.org/)