A Syntactic Approach to Type Soundness-英文文献.pdf

A Syntactic Approach to Type Soundness Andrew K Wright  Matthias Felleisen  Department of Computer Science Rice University Houston TX June Rice Technical Rep ort TR To app ear in Information and Computation Abstract We present a new approach to proving typ e soundness for HindleyMilnerstyle p olymorphic typ e systems The keys to our approach are an adaptation of sub ject reduction theorems from combinatory logic to programming languages and the use of rewriting techniques for the sp ecication of the language semantics The approach easily extends from p olymorphic functional languages to imp erative languages that provide references exceptions continuations and similar features We illustrate the technique with a typ e soundness theorem for the core of Standard ML which includes the rst typ e soundness pro of for p olymorphic exceptions and continuations Typ e Soundness Static typ e systems for programming languages attempt to prevent the o ccurrence of type errors during execution A denition of typ e error dep ends on a sp ecic language and typ e system but always includes the use of a function on arguments for which it is not dened and the attempted application of a nonfunction A static typ e system is sound if welltyp ed programs cannot cause typ e errors a programming language with a sound static typ e system is strongly typed While it is easy to design a sound typ e system for an explicitly typ ed monomorphic language the formulation of a sound typ e system for a language based on HindleyMilner style p olymorphism and typ e inference is delicate