A Semi-Syntactic Soundness Proof for HM(X)
François Pottier · 2001
This document gives a soundness proof for the generic constraint-based type inference framework HM(X). Our proof is semi-syntactic. It consists in interpreting HM(X) judgements as (sets of) judgements in an underlying type system, which is itself given a syntactic soundness proof. The former step gives a logical, intuitive view of polymorphism and constraints, yielding a concise proof. The latter is a matter of routine, because the low-level type system is simple. Thus, both logic and syntax are put to best use. 1 Introduction In approaches based on denotational semantics, types are viewed as (certain) sets of values [3, 1]. Proofs based on operational semantics, on the other hand, often oer a purely syntactic view of types, which are not given any logical interpretation [7]. In this paper, we will strike a balance between these two approaches. We start by giving a purely syntactic type system, called B(S), which enjoys a subject reduction theorem. It is described in a very ...