Higher-Order and Symbolic Computation, 14(4)387-409
From Syntactic Theories to Interpreters: Automating the Proof of Unique DecompositionYong Xiao, Department of Computer and Information Science, University of Oregon, Eugene, OR 97403, USA
Amr Sabry, Computer Science Department, Indiana University, Bloomington, IN 47405, USA
Zena M. Ariola, Department of Computer and Information Science, University of Oregon, Eugene, OR 97403, USA
|
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. Keywords: syntactic theories, interpreters, proof automation, regular tree grammars, finite tree automata |
This article can be downloaded [here].
![[picture of journal cover]](../LISP.JPG)