From Syntactic Theories to Interpreters: Automating the Proof of Unique Decomposition

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 …