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

Jean-Philippe Bernardy; Patrik Jansson

doi:10.2168/LMCS-12(2:6)2016

Jean-Philippe Bernardy ; Patrik Jansson - 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 - https://doi.org/10.2168/LMCS-12(2:6)2016

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

Authors: Jean-Philippe Bernardy ; Patrik Jansson

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.

https://doi.org/10.2168/LMCS-12(2:6)2016

Source: arXiv.org:1601.07724

Volume: Volume 12, Issue 2

Published on: June 14, 2016

Imported on: July 3, 2014

Keywords: Computer Science - Logic in Computer Science, F.4.1, F.4.2

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Publications

Has review

Review available on zbMATH Open, by Corneliu Bârsan (Snohomish) (English)

1 zbMATH Open

Bibliographic References

10 Documents citing this article

Natarajan Shankar;Zephyr Lucas, 2024, Robust Verification of PEG Parser Interpreters, 2024 IEEE Security and Privacy Workshops (SPW), pp. 180-191, 10.1109/spw63631.2024.00022.

Elton M. Cardoso;Regina De Paula;Daniel Pereira;Leonardo Reis;Rodrigo Geraldo Ribeiro, 2023, Type-based Termination Analysis for Parsing Expression Grammars, Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing, pp. 1372-1379, 10.1145/3555776.3577620.

Xiaodong Jia;Ashish Kumar;Gang Tan, 2023, A Derivative-based Parser Generator for Visibly Pushdown Grammars, ACM Transactions on Programming Languages and Systems, 45, 2, pp. 1-68, 10.1145/3591472, https://doi.org/10.1145/3591472.

Derek Egolf;Sam Lasser;Kathleen Fisher, 2022, Verbatim++: verified, optimized, and semantically rich lexing with derivatives, Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 27-39, 10.1145/3497775.3503694.

Anish Paranjpe;Gang Tan, 2021, Bohemia – A Validator for Parser Frameworks, 2021 IEEE Security and Privacy Workshops (SPW), 7, pp. 162-170, 10.1109/spw53761.2021.00030.

Clement Blaudeau;Natarajan Shankar, 2020, A verified packrat parser interpreter for parsing expression grammars, arXiv (Cornell University), pp. 3-17, 10.1145/3372885.3373836, http://arxiv.org/abs/2001.04457.

Benjamin Delaware;Sorawit Suriyakarn;Clément Pit-Claudel;Qianchuan Ye;Adam Chlipala, 2019, Narcissus: correct-by-construction derivation of decoders and encoders from binary formats, Proceedings of the ACM on Programming Languages, 3, ICFP, pp. 1-29, 10.1145/3341686, https://doi.org/10.1145/3341686.

Pierre Ganty;Boris Köpf;Pedro Valero, 2017, A Language-Theoretic View on Network Protocols, Lecture notes in computer science, pp. 363-379, 10.1007/978-3-319-68167-2_24.

Adam Sandberg Eriksson;Patrik Jansson, 2016, An agda formalisation of the transitive closure of block matrices (extended abstract), Chalmers Research (Chalmers University of Technology), pp. 60-61, 10.1145/2976022.2976025, https://research.chalmers.se/en/publication/240988.

Raul Lopes;Rodrigo Ribeiro;Carlos Camarão, 2016, Certified Derivative-Based Parsing of Regular Expressions, LA Referencia (Red Federada de Repositorios Institucionales de Publicaciones Científicas), pp. 95-109, 10.1007/978-3-319-45279-1_7, http://www.repositorio.ufop.br/handle/123456789/10509.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3050 times.

This article's PDF has been downloaded 1114 times.