Avoiding coinduction in soundness proofs

Mads Tofte's thesis uses coinduction to prove type soundness for a language with a store, because of the problem of cycles within a store: if the value in a reference cell can point to itself (such as a closure that refers to the cell that contains it), then it's not possible to find the type of a value by looking in the store. That is, type soundness involves determining the type of values, and store addresses are one kind of value. If finding the type of an address means looking up its value in the store and finding the type of that value, but that value might itself contain the same address, then typing values is not inductive.

But according to Mitch and Matthias, it's not actually necessary to use coinduction, as long as you set up the soundness hypothesis right.

The statement of subject reduction usually looks like this:

For any type environment Γ, store typing Σ, expression e, and store σ, if

1. Γ;Σ ⊢ e : τ and
2. Γ;Σ ⊢ σ and
3. e,σ → e′,σ′

then ∃ Σ′ ⊇ Σ s.t.

1. Γ;Σ ⊢ e′ : τ and
2. Γ;Σ′ ⊢ σ′.

By quantifying over all stores in the hypothesis, you can get the value of an address by simply looking it up directly in the store typing, without passing through the actual value. So the definition of Γ;Σ ⊢ σ is

dom(σ) = dom(Σ)
∀a ∈ dom(σ) . Γ;Σ ⊢ σ(a) : Σ(a)
Γ;Σ ⊢ σ

and finding the type of an address value is defined simply by looking up the address in the store typing:

     (a : τ) ∈ Σ     
Γ;Σ ⊢ a : τ ref

Update: More accurately, the hypothesis that quantifies over all stores is in the main soundness theorem:

If ∅;Σ ⊢ e : τ and ∅;Σ ⊢ σ then either

1. e,σ diverges or
2. e,σ →* v,σ′ and ∃ Σ′ s.t. ∅;Σ′ ⊢ v : t and ∅;Σ ⊢ σ′.

The proof of this theorem is a straightforward induction over the length of the reduction sequence using progress and preservation. The interesting part is that it simply assumes from the outset that we have a store σ and a store typing Σ that agree. We can easily provide an initial store ∅ and store typing ∅, which trivially agree, to get the actual proposition we want as a corollary, namely that evaluating the program in the initial store produces a well-typed result.