Statically Resolvable Ambiguity
summary
Presents a concrete solution that proves every ambiguous program in the supported formalism can be rewritten unambiguously, with a full Coq mechanization and an implementation grafted into the standard OCaml parser. Key artifacts are an isolated grouper component plus operator sequences and splittable productions that capture all ambiguity; validation parses ~1M Opam files, showing 99% of files still parse within ~12 ms and worst-case slowdown around 0.4 s, so it is both proven correct and practically fast.
AI-written summary · about
chapters (12)
- 0:00Start
- 0:32Syntactic Ambiguity in PLs
- 2:03Unresolvable Ambiguity = BAD
- 2:24Definition: Resolvable Ambiguity
- 3:31Problem and Contributions
- 5:51Intuitive (Ambiguous) Grammars
- 8:18Syntactic Composition
- 10:01Overview
- 12:37Intermediate Data
- 13:49Formal Semantics, Intuition
- 17:21The Property and the Restriction
- 19:07Benchmarks
related talks
46mMechanizing Abstract Interpretation
20mCertified Abstract Machines for Skeletal Semantics
15mTowards a Coq Specification for Generalized Algebraic Datatypes in OCaml
01h 02mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C (I...
19mInterpreting OCaml GADTs into Coq
21mVerified Extraction from Coq to OCaml
29mMetaOCaml Theory and Implementation
27mCompiling higher-order specifications to SMT solvers: how to deal with rejection ...