Transformations automatiques de specifications semantiques. Application: Un verificateur de types incremental

Laurent Hascoet INRIA, BP93, 06902 Sophia-Antipolis, France

PhD thesis, in French, 1987 (176 pages)

Abstract: The MENTOR syntax-directed editor provides a formalism to specify static semantic operations, such as type-checking, for any given language. This formalism consists of inference rules a la Plotkin. We explore here various ways of modifying those inference rules, in order to improve a type-checker. We focus on two possible improvements. One is better error recovery, the other is incremental type-checking. In the case of incremental type-checking, our method transforms a type-checker into an incremental one provided the original meets certain conditions. The conditions and why they are necessary are presented. Then we provide a partly automatic system, which does this transformation. The basic idea is a two-step method. The first step is to transform the initial algorithm, which may repeatedly traverse the syntax tree, into another one in which the tree is traversed only once, from the bottom up. The second step is to evaluate only the new error messages, i.e. the errors that were not reported on the previous type-checking.

Keywords: Semantics, Type-Checking, Inference Rules, Natural Semantics, Program transformation.

Sorry, no electronic version available.


@phdthesis{phdHascoet87,
  author = {Hasco\"et, L.},
  title = {Transformations automatiques de specifications semantiques.
           Application: Un verificateur de types incremental},
  school = {Universite de Nice Sophia-Antipolis},
  year = 1987
}