A Verified Packrat Parser Interpreter for Parsing Expression Grammars
summary
A mechanically verified packrat parser interpreter for PEGs implements a small-step semantics and a static termination analysis (computing the P0/nullable/dangerous properties) and proves soundness and completeness by building a simple reference parser and proving equivalence with an optimized packrat memoization yields linear time implementation. The development uses PVS with 329 proofs and ~4,000 input commands (88% TCCs). Semantic actions are supported via an interpretation of full parse trees, and the optimized parser is proved equivalent and practical.
AI-written summary · about
chapters (19)
- 0:00Introduction
- 0:22Contents
- 1:03What is parsing
- 2:00The passing expression grammar
- 2:55The choice operator
- 3:25The data type
- 3:42Operators
- 4:01Properties
- 6:32Failure
- 7:38Semantics
- 8:17Specification
- 9:05Wellformed
- 12:00Example
- 12:43Semantic Action
- 13:51Semantic Interpretation
- 14:58Parse
- 15:24Proof Statistics
- 17:03References
- 18:36Questions
related talks
15mA Semantic Framework for PEGs
14mFast Incremental PEG Parsing
14mA Derivative-based Parser Generator for Visibly Pushdown Grammars
44mParsing Text with a Virtual Machine
08mEverparse: A Verifying Compiler from Data Format Specifications to Verified Efficient Parsers
30mRelatively Complete Verification of Probabilistic Programs
07mParsing Expression Grammar
29mGrammar Inference for Ad Hoc Parsers