Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives
summary
Lexer based on Brzozowski derivatives moves from quadratic worst case to effectively linear time on a JSON benchmark by three verified refinements: precomputing a derivative-based transition table, memoizing maximal-prefix calls (eliminating repeated recursion), and encoding suffix keys by length in binary tries to avoid linear key reads. Implementation preserves the original correctness proofs and is verified in Coq. Benchmarks report up to a 20× speedup. Lexical rules accept user-supplied semantic actions that map labels to types and convert strings, returning None for ill-formed cases.
AI-written summary · about
chapters (8)
- 0:00Start
- 1:11Overview
- 1:27Notation - Regular Expressions
- 3:37Shortcoming #1
- 4:58Challenge - Termination
- 7:04Shortcoming #2
- 12:06Performance
- 12:46Motivating example
related talks
14mLexy: A DSL Library For C++ Parsing
01h 48mBoost.Parser (Part 2 of 2) - A Parser Combinator Library for C++
19mDerivative Based Nonbacktracking Real-World Regex Matching with Backtracking Semantics
32mTime flies like an arrow; Fruit flies like a banana: Parsers for Great Good
22mLexical Effect Handler: Fast by Design, Correct by Proof
53mSemantics-based program manipulation in the age of LLMs
27mLightweight Semantics Engineering with Redex
01h 01mExpressive Compile Time Parsers