genrest.blogg.se - Packrat definition

PACKRAT DEFINITION VERIFICATION

Sam Lasser, Chris Casinghino, Kathleen Fisher, and Cody Roux.In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, Suresh Jagannathan and Peter Sewell (Eds.). Myreen, Michael Norrish, and Scott Owens. Logical Methods in Computer Science 7, 2 (2011), 1–26. TRX: A formally verified parser interpreter. Proceedings (Lecture Notes in Computer Science), Helmut Seidl (Ed.), Vol. In Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Jacques-Henri Jourdan, François Pottier, and Xavier Leroy.In Functional Programming, Proceedings of the 1989 Glasgow Workshop, 21-23 August 1989, Fraserburgh, Scotland, UK (Workshops in Computing), Kei Davis and John Hughes (Eds.). Constructing natural language interpreters in a lazy functional language. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, Neil D. Parsing expression grammars: A recognition-based syntactic foundation. In Proceedings of the Seventh ACM SIG-PLAN International Conference on Functional Programming (ICFP ’02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002., Mitchell Wand and Simon L.

Packrat parsing: : Simple, powerful, lazy, linear time, functional pearl. Proceedings (Lecture Notes in Computer Science), Jasmin Christian Blanchette and Nikolai Kosmatov (Eds.), Vol. In Tests and Proofs - 9th International Conference, TAP 2015, Held as Part of STAF 2015, L’Aquila, Italy, July 22-24, 2015. Narcissus: Correct-byconstruction derivation of decoders and encoders from binary formats.

Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, and Adam Chlipala.

Curing the vulnerable parser: Design patterns for secure input handling.

Sergey Bratus, Lars Hermerschmidt, Sven M.

Idris, a general-purpose dependently typed programming language: Design and implementation. Proceedings (Lecture Notes in Computer Science), Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.), Vol. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. A brief overview of Agda - A functional language with dependent types.

Ana Bove, Peter Dybjer, and Ulf Norell.

Logical Methods in Computer Science 12, 2 (2016), 1–28. Certified contextfree parsing: A formalisation of Valiant’s algorithm in Agda.

Jean-Philippe Bernardy and Patrik Jansson.

In Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009 (Lecture Notes in Computer Science), Giuseppe Castagna (Ed.), Vol. Compilers: Principles, Techniques, and Tools. The proofs are formalized in mathematical terms so that similar parser interpreters can be defined in any specification language with a type system similar to PVS. Both these parser interpreters are proved equivalent to the reference one. Building on the reference parser interpreter, we define a packrat parser interpreter as well as an extension that is capable of semantic interpretation. The correctness properties are embedded in the types of the operations so that the proofs can be easily constructed from local proof obligations. Rather than relying on an inductive definition of parsing, we use abstract syntax trees that represent the computational trace of the parser to provide an effective proof certificate for correct parsing and ensure that parsing properties including soundness and completeness are maintained. In order to ensure termination of parsing, we define a notion of a well-formed grammar.

PACKRAT DEFINITION VERIFICATION

We use the rich type system of the PVS specification language and verification system to formalize the metatheory of PEGs and define a reference implementation of a recursive parser interpreter for PEGs. PEGs are expressive, unambiguous, and efficient to parse in a top-down recursive descent style. Parsing expression grammars (PEGs) offer a natural opportunity for building verified parser interpreters based on higher-order parsing combinators.