Bernardy, Jean-Philippe and Jansson, Patrik - Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda

lmcs:1638 - Logical Methods in Computer Science, June 14, 2016, Volume 12, Issue 2
Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda

Authors: Bernardy, Jean-Philippe and Jansson, Patrik

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.


Source : oai:arXiv.org:1601.07724
DOI : 10.2168/LMCS-12(2:6)2016
Volume: Volume 12, Issue 2
Published on: June 14, 2016
Submitted on: July 3, 2014
Keywords: Computer Science - Logic in Computer Science,F.4.1,F.4.2


Share

Consultation statistics

This page has been seen 111 times.
This article's PDF has been downloaded 148 times.