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 σ, ifBy 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
then ∃ Σ′ ⊇ Σ s.t.
- Γ;Σ ⊢ e : τ and
- Γ;Σ ⊢ σ and
- e,σ → e′,σ′
- Γ;Σ ⊢ e′ : τ and
- Γ;Σ′ ⊢ σ′.
and finding the type of an address value is defined simply by looking up the address in the store typing:
dom(σ) = dom(Σ)
∀a ∈ dom(σ) . Γ;Σ ⊢ σ(a) : Σ(a)
Γ;Σ ⊢ σ
(a : τ) ∈ Σ
Γ;Σ ⊢ a : τ ref
Update: More accurately, the hypothesis that quantifies over all stores is in the main soundness theorem:
If ∅;Σ ⊢ e : τ and ∅;Σ ⊢ σ then eitherThe 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.
- e,σ diverges or
- e,σ →* v,σ′ and ∃ Σ′ s.t. ∅;Σ′ ⊢ v : t and ∅;Σ ⊢ σ′.