Type Soundness Proofs

Presented by Richard C. Cobbe
Transcribed by Vasileios Koutavas

 

Milner 1978

Used a categorical proof technique to prove the soundness of polymorphic type inference for the functional core of ML.

Some of the domains that he used:
    V: domain of tagged values (disjoint union)
    B0: Boolean Domain

Types:
    i0, i1, ... : ground types
    t -> t : function types

Relation: u "has type" t
    |= u: t

bottom has every type
WRONG has no type

* The relation |= looks like a logical relation. It relates the type meaning of the term to its actual meaning.

Environments:
    r: semantic environment
    G: type environment

Relation between environments (compatible environments, or "r respects G"):
    for all x in dom(r),     |= r(x): G(x)

This can also be written:
|= r: G

Soundness Theorem:
   
If |= r: G and G |- e: t, then |= E[[e]] r: t

Proof: structural induction

one case of the induction:

G |- e = if e1 then e2 else e3 : t

v1 = E[[e1]] r
    - v1 = WRONG, then not typable
    - v1 = bottom, bottom has all types => well typed
    - v1 = B0 (boolean), then pick e1 or e2

* This was the first paper that introduced type soundness.

 

Damas 1985

Extended the proof technique for imperative languages. It resulted to a very complicated categorical proof that it was difficult to follow and verify.

 

Tofte 1989

Used big-step operational semantics for a functional language with references:

s, r |- e \Downarrow v, s'

Proof method:

Step 1:
If |= r: G and G |- e: t and s, r |- e \Downarrow v, s' then |= v: t

problem: not enough information. There is no store information

Step 2: Add store in the typing relations
If s |= r: G and G |- e: t and s, r |- e \Downarrow v, s' then s |= v: t

problem: There is no store type information.
e.g. This scenario is allowed:
    s = { a -> nil }
    r = { x -> a, y -> a }
    G = { x -> (int list) ref, y -> (bool list) ref }

    e = x := [7]; !y

Step 3: Add store typing ST: loc -> types

Soundness Theorem:
If s: ST |= r: G and G |- e: t and s, r |- e \Downarrow v, s' then there exists ST' s.t. s': ST' |= v: t

The definition of the relation s: ST |= r: G is not trivial. Because of possible cycles in the store an inductive definition is not well-founded. We need a co-inductive set for the definition of this relation (Maximal fixpoint):

We have to find a set of values and prove that this set is consistent with the function F(Q): Q subset or equal to F(Q). (definition of function in the paper)

s: ST |= v: t ==> s': ST' |= v: t
where:
    s' = s + { a0 -> v0 }
    ST' = ST + { a0 -> t0 } let Q = { (s': ST' |= v: t) | s: ST |= v: t }

We have to show that: Q subset or equal to F(Q) (Q is F-consistent)

* Co-induction seems easier than categorical proof, but it has the difficulty to guess the initial set Q.
* Advantage of this method over Milner's: It avoids the complicated domain construction.

 

Wright and Felleisen 1992

Presented a proof technique based on small-step semantics.

Soundness Theorem:
If |- e: t then e diverges or e |->> v and |- v: t

where |->> is the transitive closure of small-step reduction (->), inside a context.

Proof:
It is undecidable if a term will get stuck. Therefore we use a conservative approximation for stuck terms, called Faulty Terms:
(c v) s.t delta(c, v) is undefined

The proof is based on three lemmas:

Lemma 1: Subject Reduction (Preservation)
If G |- e1: t and e1 -> e2 then G |- e2: t1

Proof: case analysis on the form of small step reduction (->)

Corollary:
 If G |- e1: t and e1 |->> e2 then G |- e2: t1

Lemma 2: Uniform Evaluation (not Progress)
For closed e, if there is no faulty e' s.t. e |->> e' then e diverges or e |->> v

Lemma 3: Faulty terms are untypable.

Proof: straight forward case analysis on delta(c, v)

From lemmas 1,2,3 we get the proof of the soundness theorem.

Extensibility of the proof:
In the paper the language is extended with references. The new soundness proof reuses the cases of the old proof an adds only the new cases in the three lemmas.

Also we have to add the new faulty terms (they expand quadratically):
(! v) when v is not a reference
(:= v) when v is not a reference
(\ro \theta <x, v>. (x v))

Q: Why is Wright & Felleisen's technique better?
    - Milner's technique: difficult domain construction
    - Tofte's technique: difficult co-induction
    - Wright & Felleisen's technique: (a) straight forward induction, (b) extensible.