Paper Info
Title
From Syntactic Theories to Interpreters: Automating the Proof of Unique Decomposition
Abstract
Developing syntactic theories for reasoning about programming languages usually involves proving a unique-decomposition lemma. The proof of such a lemma is tedious, error-prone, and is usually attempted many times during the design of a theory. We therefore investigate the automation of such proofs.We map the unique-decomposition lemma to the problems of checking equivalence and ambiguity of syntactic definitions. Because checking these properties of context-free grammars is undecidable, we work with regular tree grammars and use algorithms on finite tree automata to perform the checking. To make up for the insufficient expressiveness of regular tree grammars, we extend the basic framework with built-in types and constants, contexts, and polymorphic types.Our implementation extends an earlier system by Xiao et al. [16] that translates semantic specifications expressed as syntactic theories to interpreters. We have successfully used the combined system to generate interpreters and verify the unique-decomposition lemma for a number of examples.
Year
DOI
Venue
2001
10.1023/A:1014408032446
Higher-Order and Symbolic Computation
Keywords
Field
DocType
built-in type,context-free grammar,finite tree automata,syntactic theories,proof automation,regular tree grammar,finite tree automaton,basic framework,unique-decomposition lemma,regular tree grammars,earlier system,syntactic theory,combined system,unique decomposition,syntactic definition,interpreters,programming language
Rule-based machine translation,Context-free grammar,Programming language,Computer science,Mathematical proof,Pumping lemma for context-free languages,Parsing,Regular language,Syntax,Lemma (mathematics)
Journal
Volume
Issue
ISSN
14
4
1573-0557
Citations 
PageRank 
References 
9
0.65
9
Authors
3
Name
Order
Citations
PageRank
Yong Xiao190.65
Amr Sabry252035.46
Zena M. Ariola348238.61