Lay-it-out: Interactive Design of Layout-Sensitive Grammars
Fengmin Zhu, Jiangyi Liu, Fei He

TL;DR
Lay-it-out is an interactive framework that helps design layout-sensitive grammars by refining ambiguous grammars with user input and automatically generating example sentences, supported by formal proofs.
Contribution
It introduces a novel interactive approach for designing layout-sensitive grammars with SMT-based synthesis and formal verification in Coq.
Findings
Successfully refines ambiguous grammars with user interaction.
Automatically generates example sentences using SMT solving.
Demonstrates practicality and scalability on real grammars.
Abstract
Layout-sensitive grammars have been adopted in many modern programming languages. However, tool support for this kind of grammars still remains limited and immature. In this paper, we present Lay-it-out, an interactive framework for layout-sensitive grammar design. Beginning with a user-defined ambiguous grammar, our framework refines it by synthesizing layout constraints through user interaction. For ease of interaction, a shortest nonempty ambiguous sentence (if exists) is automatically generated by our bounded ambiguity checker via SMT solving. The soundness and completeness of our SMT encoding are mechanized in the Coq proof assistant. Case studies on real grammars, including a full grammar, demonstrate the practicality and scalability of our approach.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Software Engineering Research · Software Testing and Debugging Techniques
