×

zbMATH — the first resource for mathematics

Certified CYK parsing of context-free languages. (English) Zbl 1371.68137
Summary: We report a work on certified parsing for context-free grammars. In our development we implement the Cocke-Younger-Kasami parsing algorithm and prove it correct using the Agda dependently typed programming language.

MSC:
68Q42 Grammars and rewriting systems
68N15 Theory of programming languages
68Q45 Formal languages and automata
Software:
Agda; TRX
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Firsov, D.; Uustalu, T., Certified parsing of regular languages, (Gonthier, G.; Norrish, M., Proc. of 3rd Int. Conf. on Certified Programs and Proofs, CPP 2013, Lect. Notes Comput. Sci., vol. 8307, (2013), Springer Berlin), 98-113 · Zbl 1303.68077
[2] Norell, U., Towards a practical programming language based on dependent type theory, (2007), Chalmers University of Technology Göteborg, Ph.D. thesis
[3] Norell, U., Dependently typed programming in agda, (Koopman, P.; Plasmeijer, R.; Swierstra, S. D., Revised Lectures from 6th Int. School on Advanced Functional Programming, AFP 2009, Lect. Notes Comput. Sci., vol. 5832, (2009), Springer Berlin), 230-266 · Zbl 1263.68038
[4] Younger, D., Recognition and parsing of context-free languages in time \(O(n^3)\), Inf. Comput., 10, 2, 189-208, (1967) · Zbl 0149.24803
[5] Valiant, L. G., General context-free recognition in less than cubic time, J. Comput. Syst. Sci., 10, 2, 308-314, (1975) · Zbl 0312.68042
[6] Nordström, B., Terminating general recursion, BIT Numer. Math., 28, 3, 605-619, (1988) · Zbl 0659.68020
[7] Wadler, P., Comprehending monads, (Proc. of 1990 ACM Conf. on LISP and Functional Programming, LFP ’90, (1990), ACM New York), 61-78
[8] Barthwal, A.; Norrish, M., Verified, executable parsing, (Castagna, G., Proc. of 18th Europ. Symp. on Programming Languages and Systems, ESOP ’09, Lect. Notes Comput. Sci., vol. 5502, (2009), Springer Berlin), 160-174 · Zbl 1234.68359
[9] Koprowski, A.; Binsztok, H., TRX: a formally verified parser interpreter, Log. Methods Comput. Sci., 7, 2, (2011), art. no. 18 · Zbl 1260.68194
[10] Jourdan, J.-H.; Pottier, F.; Leroy, X., Validating LR(1) parsers, (Seidl, H., Proc. of 21st Europ. Symp. on Programming, ESOP 2012, Lect. Notes Comput. Sci., vol. 7211, (2012), Springer Berlin), 397-416 · Zbl 1352.68131
[11] Danielsson, N. A., Total parser combinators, (Proc. of 15th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP ’10, (2010), ACM New York), 285-296 · Zbl 1323.68330
[12] Sjöblom, T. B., An agda proof of the correctness of Valiant’s algorithm for context free parsing, (2013), Chalmers University of Technology Göteborg, Master’s thesis
[13] Ridge, T., Simple, functional, sound and complete parsing for all context-free grammars, (Jouannaud, J.-P.; Shao, Z., Proc. of 1st Int. Conf. on Certified Programs and Proofs, CPP 2011, Lect. Notes Comput. Sci., vol. 7086, (2011), Springer Berlin), 103-118 · Zbl 1350.68164
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.