Dissertation Defense Details
From Syntactic Theories to Interpreters: Specifying and Proving Properties
| Author: | Yong Xiao |
|---|---|
| Date: | May 10, 2004 |
| Time: | 09:30 |
| Location: | 220 Deschutes |
| Committee: | Zena Ariola (Chair) Andrzej Proskurowski Chris Wilson Sergey Yuzvinsky |
Abstract
Syntactic theories have been developed to reason about many aspects of modern programming languages. Experience shows taht the development of such theories is error-prone. In order to ensure that the theories are sensible, many properties need to be checked. For example, we need to know if there is always a rule to rewrite a valid program, and if a unique value can be obtained by evaluating the rules (which is described by a unique-decomposition lemma) and if the type of a program is preserved during evaluation (which is described by a subject reduction lemma). In many situations, the proofs of these properties do not require deep insight. However, many purported proofs suffer from being incomplete and often the missed case is the most problematic one. Thus, we think that in order to rely on syntactic theories, it is of mandatory importance to design tools that support their development. The work described in this thesis offers a first step in that direction
We introduce a specification language, SL language, which can have direct and concise representation of syntactic theories and their properties. We also introduce the SL system which can automatically generate interpreters from SL specification and automatically prove some properties such as unique decomposition and subject reduction.