Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda

TL;DR

This paper formalizes and verifies a generalized version of Valiant's algorithm for context-free language recognition using Agda, providing a certified, algebraic approach with potential applications in parsing and matrix operations.

Contribution

It introduces a formal, verified algebraic specification and implementation of a generalized Valiant's algorithm in Agda, with correctness proof.

Findings

Certified correctness proof in Agda.

Generalization applicable to recognition, parsing, and matrix transitive closure.

State-of-the-art formalization and proof techniques demonstrated.

Abstract

Valiant (1975) has developed an algorithm for recognition of context free languages. As of today, it remains the algorithm with the best asymptotic complexity for this purpose. In this paper, we present an algebraic specification, implementation, and proof of correctness of a generalisation of Valiant's algorithm. The generalisation can be used for recognition, parsing or generic calculation of the transitive closure of upper triangular matrices. The proof is certified by the Agda proof assistant. The certification is representative of state-of-the-art methods for specification and proofs in proof assistants based on type-theory. As such, this paper can be read as a tutorial for the Agda system.