Automated Ambiguity Detection in Layout-Sensitive Grammars

Explore a 17-minute video presentation from OOPSLA2 2023 conference that delves into automated ambiguity detection in layout-sensitive grammars. Learn about the novel approach developed by researchers from Tsinghua University to tackle this challenging problem in programming language design. Discover how they extend previous work on context-free grammar ambiguity detection to layout-sensitive grammars using SMT solving. Understand the key innovation of a reachability condition that carefully considers layout constraints' impact on ambiguity. Gain insights into the equivalent ambiguity notion called local ambiguity and its SMT encoding. See how the researchers developed a bounded ambiguity checker to find the shortest nonempty ambiguous sentence in user-input grammars. Examine the evaluation results on grammar fragments and full grammars from languages like YAML and Python, demonstrating the effectiveness of this approach. The presentation also covers the mechanized soundness and completeness proofs in the Coq proof assistant, providing a robust theoretical foundation for the work.