Presented by Richard C. Cobbe

Transcribed by Vasileios Koutavas

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.

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

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.

**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

(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.