COMPSCI 3MI3 : Assignment 9
Fall 2021
Nicholas Moore
1. (12 points) Progress of Reference Semantics
In topic 10, we presented the following definition of progress, which had to be redefined with our inclu-
sion of µ and Σ in our calculus.
THEOREM: [Progress]
Suppose t to be a closed, well typed term (that is, Ø | Σ ` t : T for some T and Σ). Then either t is a
value, or else, for any store µ such that Ø |Σ ` µ, there is some term t′ and store µ′ such that t |µ→ t′ |µ′.
Proof Sketch
• Straightforward induction on typing derivations, following the pattern established in topic 8.
• The canonical forms lemma needs two additional cases, stating that all values of type Ref T are
locations, and similarly for Unit.
Produce a proof of progress for simply typed λ calculus, augmented with Unit, the sequencing operator,
and our operations on references. You do not need to reprove parts of the calculus which have not
changed, but you do need to state that they haven’t changed, and that the theorem still holds for them.
As noted above, you need to add a couple cannonical forms. Include these new canonnical forms (you
don’t have to prove them).
2. (14 points) Preservation of Reference Semantics.
In topic 10, we developed the following definition of preservation.
THEOREM: [Preservation]
(Γ | Σ ` t : T ) ∧ (t | µ→ t′ | µ′) ∧ (Γ | Σ ` µ) =⇒ (∃Σ′ ⊇ Σ | (Γ | Σ′ ` t′ : T ) ∧ (Γ | Σ′ ` µ′)) (1)
Proof Sketch Of Preservation
• Straightforward induction on evaluation derivations, using the provided lemmas, plus the inversion
property of our new typing rules (itself a straightforward extension of the inversion lemma of simply
typed λ-Calculus).
In order to prove preservation, we will need the following three technical lemmas.
LEMMA: [Preservation Over Substitution]
(Γ, x : S | Σ ` t : T ) ∧ (Γ | Σ ` s : S) =⇒ (Γ | Σ ` [x 7→ s]t : T ]) (2)
LEMMA: [Preservation Over Storage]
(Γ | Σ ` µ) ∧ (Σ(l) = T ) ∧ (Γ | Σ ` v : T ) =⇒ (Γ | Σ ` [l 7→ v]µ)) (3)
LEMMA: [Weakening Over Typing Stores]
(Γ | Σ ` t : T ) ∧ (Σ′ ⊇ Σ) =⇒ (Γ | Σ′ ` t : T ) (4)
Give a proof of preservation as defined above, over simply typed λ-Calculus, augmented with Unit, the
sequencing operator, and our operations on references. You may use the lemmas above without needing
to prove them. The inversion lemmas described should be formally stated, but no proof need be given
of them.
Once again, you do not need to reprove parts of the calculus which have not changed, but you do need
to state that they haven’t changed, and that the theorem holds for them.







































学霸联盟