# References: Typing Mutable References

So far, we have considered a variety of
Most practical programming languages also include various
In this chapter, we'll see how one sort of computational
effect---mutable references---can be added to the calculi we have
studied. The main extension will be dealing explicitly with a
We need to repeat the definition of the solve by inversion
tactic here so that we don't need to import all of Stlc.v. It
really belongs in SfLib.v.

*pure*language features, including functional abstraction, basic types such as numbers and booleans, and structured types such as records and variants. These features form the backbone of most programming languages---including purely functional languages such as Haskell, ``mostly functional'' languages such as ML, imperative languages such as C, and object-oriented languages such as Java.*impure*features that cannot be described in the simple semantic framework we have used so far. In particular, besides just yielding results, evaluation of terms in these languages may assign to mutable variables (reference cells, arrays, mutable record fields, etc.), perform input and output to files, displays, or network connections, make non-local transfers of control via exceptions, jumps, or continuations, engage in inter-process synchronization and communication, and so on. In the literature on programming languages, such ``side effects'' of computation are more generally referred to as*computational effects*.*store*(or*heap*). This extension is straightforward to define; the most interesting part is the refinement we need to make to the statement of the type preservation theorem.### Preliminaries

Tactic Notation "solve_by_inversion_step" tactic(t) :=

match goal with

| H : _ |- _ => solve [ inversion H; subst; t ]

end

|| fail "because the goal is not solvable by inversion.".

Tactic Notation "solve" "by" "inversion" "1" :=

solve_by_inversion_step idtac.

Tactic Notation "solve" "by" "inversion" "2" :=

solve_by_inversion_step (solve by inversion 1).

Tactic Notation "solve" "by" "inversion" "3" :=

solve_by_inversion_step (solve by inversion 2).

Tactic Notation "solve" "by" "inversion" :=

solve by inversion 1.

### Records

*records*. Intuitively, these are n-ary products with labeled fields.

t ::= Terms: | ... | {i1=t1, ..., in=tn} record | t.i projection v ::= Values: | ... | {i1=v1, ..., in=vn} record value T ::= Types: | ... | {i1:T1, ..., in:Tn} record typeIntuitively, the generalization is pretty obvious. But it's worth noticing that what we've actually written is rather informal: in particular, we've written "..." in several places to mean "any number of these," and we've omitted explicit mention of the usual side-condition that the labels of a record should not contain repetitions. It is possible to devise informal notations that are more precise, but these tend to be quite heavy and to obscure the main points of the definitions. So we'll leave these a bit loose here (they are informal anyway, after all) and do the work of tightening things up elsewhere (in Records.v).

ti --> ti' | (ST_Rcd) |

{i1=v1, ..., im=vm, in=ti, ...} --> | |

{i1=v1, ..., im=vm, in=ti', ...} |

t1 --> t1' | (ST_Proj1) |

t1.i --> t1'.i |

(ST_ProjRcd) | |

{..., i=vi, ...}.i --> vi |

Gamma |- t1 : T1 ... Gamma |- tn : Tn | (T_Rcd) |

Gamma |- {i1=t1, ..., in=tn} : {i1:T1, ..., in:Tn} |

Gamma |- t : {..., i:Ti, ...} | (T_Proj) |

Gamma |- t.i : Ti |

### Encoding Records

- We can directly formalize the syntactic forms and inference
rules, staying as close as possible to the form we've given
them above. This is conceptually straightforward, and it's
what we'd want to do if we were building a real compiler -- in
particular, it will allow is to print error messages in the
form that programmers will find easy to understand. But the
formal versions of the rules will not be very pretty!
- We could look for a smoother way of presenting records -- for
example, a binary presentation with one constructor for the
empty record and another constructor for adding a single field
to an existing record, instead of a single monolithic
constructor that builds a whole record at once. This is the
right way to go if we are primarily interested in studying the
metatheory of the calculi with records, since it leads to
clean and elegant definitions and proofs. The file Records.v
shows how this can be done.
- Alternatively, if we like, we can avoid formalizing records altogether, by stipulating that record notations are just informal shorthands for more complex expressions involving pairs and product types. We sketch this approach here.

{} ----> unit {t1, t2, ..., tn} ----> (t1, trest) where {t2, ..., tn} ----> trestSimilarly, we can encode tuple types using nested product types:

{} ----> Unit {T1, T2, ..., Tn} ----> (T1, TRest) where {T2, ..., Tn} ----> TRestThe operation of projecting a field from a tuple can be encoded using a sequence of second projections followed by a first projection:

t.0 ----> t.fst t.(n+1) ----> (t.snd).n

*position*of the label. For example, we might assign positions like this:

LABEL POSITION a 0 b 1 c 2 ... ... foo 1004 ... ... bar 10562 ... ...

{a=5, b=6} ----> {5,6} {a=5, c=7} ----> {5,unit,7} {c=7, a=5} ----> {5,unit,7} {c=5, b=3} ----> {unit,3,5} {f=8,c=5,a=7} ----> {7,unit,5,unit,unit,8} {f=8,c=5} ----> {unit,unit,5,unit,unit,8}Note that each field appears in the position associated with its label, that the size of the tuple is determined by the label with the highest position, and that we fill in unused positions with unit.

{a:Nat, b:Nat} ----> {Nat,Nat} {c:Nat, a:Nat} ----> {Nat,Unit,Nat} {f:Nat,c:Nat} ----> {Unit,Unit,Nat,Unit,Unit,Nat}

t.l ----> t.(position of l)

*choose*the numbering of labels so that we assign small positions to the most frequently used labels. Indeed, there are industrial compilers that essentially do this!

# Mutable References

*value*is the number 5, or we can have a variable y whose value is a

*reference*(or

*pointer*) to a mutable cell whose current contents is 5, and the difference is visible to the programmer. We can add x to another number, but not assign to it. We can use y directly to assign a new value to the cell that it points to (by writing y:=84), but we cannot use it directly as an argument to plus. Instead, we must explicitly

*dereference*it, writing !y to obtain its current contents.

*every*variable name refers to a mutable cell, and the operation of dereferencing a variable to obtain its current contents is implicit.

*store*(or

*heap*). This extension is straightforward to define; the most interesting part is the refinement we need to make to the statement of the type preservation theorem.

## Syntax

The basic operations on references are
We will start with the simply typed lambda calculus over the
natural numbers. To the base natural number type and arrow types
we need to add two more types to deal with references. First, we
need the

*allocation*,*dereferencing*, and*assignment*.- To allocate a reference, we use the ref operator, providing
an initial value for the new cell. For example, ref 5
creates a new cell containing the value 5, and evaluates to
a reference to that cell.
- To read the current value of this cell, we use the
dereferencing operator !; for example, !(ref 5) evaluates
to 5.
- To change the value stored in a cell, we use the assignment
operator. If r is a reference, r := 7 will store the
value 7 in the cell referenced by r. However, r := 7
evaluates to the trivial value unit; it exists only to have
the
*side effect*of modifying the contents of a cell.

### Types

*unit type*, which we will use as the result type of an assignment operation. We then add*reference types*. If T is a type, then Ref T is the type of references which point to a cell holding values of type T.Inductive ty : Type :=

| ty_nat : ty

| ty_arrow : ty -> ty -> ty

| ty_unit : ty

| ty_ref : ty -> ty.

### Terms

- tm_ref t1, informally written ref t1, allocates a new
reference cell with the value t1 and evaluates to the
location of the newly allocated cell;
- tm_deref t1, informally !t1, evaluates to the contents of
the cell referenced by t1;
- tm_assign t1 t2, informally t1 := t2, assigns t2 to the
cell referenced by t1; and
- tm_loc l represents a reference to the cell at location l. We'll discuss locations later.

Inductive tm : Type :=

| tm_var : id -> tm

| tm_app : tm -> tm -> tm

| tm_abs : id -> ty -> tm -> tm

| tm_nat : nat -> tm

| tm_succ : tm -> tm

| tm_pred : tm -> tm

| tm_mult : tm -> tm -> tm

| tm_if0 : tm -> tm -> tm -> tm

(* New terms: *)

| tm_unit : tm

| tm_ref : tm -> tm

| tm_deref : tm -> tm

| tm_assign : tm -> tm -> tm

| tm_loc : nat -> tm.

Tactic Notation "tm_cases" tactic(first) tactic(c) :=

first;

[ c "tm_var" | c "tm_app" | c "tm_abs"

| c "tm_zero" | c "tm_succ" | c "tm_pred" | c "tm_mult" | c "tm_if0"

| c "tm_unit" | c "tm_ref" | c "tm_deref"

| c "tm_assign" | c "tm_loc"

].

Definition _x := Id 0.

Definition _y := Id 1.

Definition _r := Id 2.

Definition _s := Id 3.

### Typing (Preview)

Gamma |- t1 : T1 | (T_Ref) |

Gamma |- ref t1 : Ref T1 |

Gamma |- t1 : Ref T11 | (T_Deref) |

Gamma |- !t1 : T11 |

Gamma |- t1 : Ref T11 | |

Gamma |- t2 : T11 | (T_Assign) |

Gamma |- t1 := t2 : Unit |

### Values and Substitution

Inductive value : tm -> Prop :=

| v_abs : forall x T t,

value (tm_abs x T t)

| v_nat : forall n,

value (tm_nat n)

| v_unit :

value tm_unit

| v_loc : forall l,

value (tm_loc l).

Hint Constructors value.

Extending substitution to handle the new syntax of terms is
straightforward.

Fixpoint subst (x:id) (s:tm) (t:tm) : tm :=

match t with

| tm_var x' => if beq_id x x' then s else t

| tm_app t1 t2 => tm_app (subst x s t1) (subst x s t2)

| tm_abs x' T t1 => if beq_id x x' then t else tm_abs x' T (subst x s t1)

| tm_nat n => t

| tm_succ t1 => tm_succ (subst x s t1)

| tm_pred t1 => tm_pred (subst x s t1)

| tm_mult t1 t2 => tm_mult (subst x s t1) (subst x s t2)

| tm_if0 t1 t2 t3 => tm_if0 (subst x s t1) (subst x s t2) (subst x s t3)

| tm_unit => t

| tm_ref t1 => tm_ref (subst x s t1)

| tm_deref t1 => tm_deref (subst x s t1)

| tm_assign t1 t2 => tm_assign (subst x s t1) (subst x s t2)

| tm_loc _ => t

end.

## Pragmatics

### Side Effects and Sequencing

*sequencing*. For example, we can write

r:=succ(!r); !ras an abbreviation for

(\x:Unit. !r) (r := succ(!r)).This has the effect of evaluating two expressions in order and returning the value of the second. Restricting the type of the first expression to Unit helps the typechecker to catch some silly errors by permitting us to throw away the first value only if it is really guaranteed to be trivial.

r:=succ(!r); r:=succ(!r); r:=succ(!r); r:=succ(!r); !r

(If we were building a full-blown programming language
instead of just a theoretical model, this derived form could be
implemented by giving the parser a separate rule for expressions
of the form t1;t2 but expanding such expressions into an
abstraction and an application instead of defining a separate
tm_seq constructor for the abstract syntax tree datatype.)
It is important to bear in mind the difference between the
If we make a copy of r, for example by binding its value to
another variable s, what gets copied is only the
For example, after evaluating
The possibility of aliasing can make programs with references
quite tricky to reason about. For example, the expression
Of course, aliasing is also a large part of what makes references
useful! In particular, it allows us to set up "implicit
communication channels"---shared state---between different parts
of a program.
The possibility of aliasing can make programs with references
quite tricky to reason about. For example, the expression (r:=1;
r:=!s), which assigns 1 to r and then immediately overwrites
it with s's current value, has exactly the same effect as the
single assignment r:=!s,
Of course, aliasing is also a large part of what makes references
useful. In particular, it allows us to set up ``implicit
communication channels''---shared state---between different parts
of a program. For example, suppose we define a reference cell and
two functions that manipulate its contents:
In the context of these declarations, calling incc results in
changes to c that can be observed by calling decc. For
example, if we replace the ... with (incc unit; incc unit; decc
unit), the result of the whole program will be 1.
We can go a step further and write a

### References and Aliasing

*reference*that is bound to r and the*cell*in the store that is pointed to by this reference.*reference*, not the contents of the cell itself.let r = ref 5 in let s = r in s := 82; (!r)+1the cell referenced by r will contain the value 82, which will also be the result of the whole expression. The references r and s are said to be

*aliases*for the same cell.r := 1; r := !sassigns 1 to r and then immediately overwrites it with s's current value; this has exactly the same effect as the single assignment

r:=!s

*unless*we happen to do it in a context where r and s are aliases for the same cell!### Shared State

*unless*we write it in a context where r and s are aliases for the same cell.let c = ref 0 in let incc = \_:Unit. (c := succ (!c); !c) in let decc = \_:Unit. (c := pred (!c); !c) in ...Note that, since their argument types are Unit, the abstractions in the definitions of incc and decc are not providing any useful information to the bodies of the functions (using the wildcard _ as the name of the bound variable is a reminder of this). Instead, their purpose is to "slow down" the execution of the function bodies: since function abstractions are values, the two lets are executed simply by binding these functions to the names incc and decc, rather than by actually incrementing or decrementing c. Later, each call to one of these functions results in its body being executed once and performing the appropriate mutation on c. Such functions are often called

*thunks*.### Objects

*function*that creates c, incc, anbd decc, packages incc and decc together into a record, and returns this record:newcounter = \_:Unit. let c = ref 0 in let incc = \_:Unit. (c := succ (!c); !c) in let decc = \_:Unit. (c := pred (!c); !c) in {i=incc, d=decc}Now, each time we call newcounter, we get a new record of functions that share access to the same storage cell c. The caller of newcounter can't get at this storage cell directly, but can affect it indirectly by calling the two functions. In other words, we've created a simple form of

*object*.let c1 = newcounter unit in let c2 = newcounter unit in // Note that we've allocated two separate storage cells now! let r1 = c1.i unit in let r2 = c2.i unit in r2 // yields 1, not 2!

#### Exercise: 1 star

Draw (on paper) the contents of the store at the point in execution where the first two lets have finished and the third one is about to begin.
(* FILL IN HERE *)

☐
A reference cell need not contain just a number: the primitives
we've defined above allow us to create references to values of any
type, including functions. For example, we can use references to
functions to give a (not very efficient) implementation of arrays
of numbers, as follows. Write NatArray for the type
Ref (Nat->Nat).
Begin by defining a useful helper function:

### References to Compound Types

equal = fix (\eq:Nat->Nat->Bool. \m:Nat. \n:Nat. if m=0 then iszero n else if n=0 then false else eq (pred m) (pred n))Now, to build a new array, we allocate a reference cell and fill it with a function that, when given an index, always returns 0.

newarray = \_:Unit. ref (\n:Nat.0)To look up an element of an array, we simply apply the function to the desired index.

lookup = \a:NatArray. \n:Nat. (!a) nThe interesting part of the encoding is the update function. It takes an array, an index, and a new value to be stored at that index, and does its job by creating (and storing in the reference) a new function that, when it is asked for the value at this very index, returns the new value that was given to update, and on all other indices passes the lookup to the function that was previously stored in the reference.

update = \a:NatArray. \m:Nat. \v:Nat. let oldf = !a in a := (\n:Nat. if equal m n then v else oldf n);References to values containing other references can also be very useful, allowing us to define data structures such as mutable lists and trees.

#### Exercise: 2 stars

If we defined update more compactly like thisupdate = \a:NatArray. \m:Nat. \v:Nat. a := (\n:Nat. if equal m n then v else (!a) n)would it behave the same?

(* FILL IN HERE *)

☐
A last issue that we should mention before we move on with
formalizing references is storage

### Garbage Collection

*de*-allocation. We have not provided any primitives for freeing reference cells when they are no longer needed. Instead, like many modern languages (including ML and Java) we rely on the run-time system to perform*garbage collection*, collecting and reusing cells that can no longer be reached by the program. This is*not*just a question of taste in language design: it is extremely difficult to achieve type safety in the presence of an explicit deallocation operation. The reason for this is the familiar*dangling reference*problem: we allocate a cell holding a number, save a reference to it in some data structure, use it for a while, then deallocate it and allocate a new cell holding a boolean, possibly reusing the same storage. Now we can have two names for the same storage cell---one with type Ref Nat and the other with type Ref Bool.#### Exercise: 1 star

Show how this can lead to a violation of type safety.
(* FILL IN HERE *)

☐
The most subtle aspect of the treatment of references appears when
we consider how to formalize their operational behavior. One way
to see why is to ask, ``What should be the
What, then, is a reference?
The run-time store in most programming language implementations is
essentially just a big array of bytes. The run-time system keeps track
of which parts of this array are currently in use; when we need to
allocate a new reference cell, we allocate a large enough segment from
the free region of the store (4 bytes for integer cells, 8 bytes for
cells storing Floats, etc.), mark it as being used, and return the
index (typically, a 32- or 64-bit integer) of the start of the newly
allocated region. These indices are references.
For present purposes, there is no need to be quite so concrete.
We can think of the store as an array of
(Treating locations abstractly in this way will prevent us from
modeling the
Recall that, in the small-step operational semantics for
IMP, the step relation needed to carry along an auxiliary state in
addition to the program being executed. In the same way, once we
have added reference cells to the STLC, our step relation must
carry along a store to keep track of the contents of reference
cells.
We could reuse the same functional representation we used for
states in IMP, but for carrying out the proofs it is actually more
convenient to simply use a list of values to represent stores. In
IMP, the programmer could decide which variable to modify, so
states had to be ready to map any collection of variables to
values. However, in the STLC with references, the programmer has
no control over which location is used for a new reference; the
only way to create a reference cell is with tm_ref t1, which
puts the value t1 in a new reference cell and evaluates to the
location of the reference cell it has chosen. So we can just add
a new reference cell to the end of the list representing the store
each time a tm_ref is encountered.

## Operational Semantics

### Locations

*values*of type Ref T?'' The crucial observation that we need to take into account is that evaluating a ref operator should*do*something---namely, allocate some storage---and the result of the operation should be a reference to this storage.*values*, rather than an array of bytes, abstracting away from the different sizes of the run-time representations of different values. A reference, then, is simply an index into the store. (If we like, we can even abstract away from the fact that these indices are numbers, but for purposes of formalization in Coq it is a bit more convenient to use numbers.) We'll use the word*location*instead of*reference*or*pointer*from now on to emphasize this abstract quality.*pointer arithmetic*found in low-level languages such as C. This limitation is intentional. While pointer arithmetic is occasionally very useful, especially for implementing low-level components of run-time systems, such as garbage collectors, it cannot be tracked by most type systems: knowing that location n in the store contains a float doesn't tell us anything useful about the type of location n+4. In C, pointer arithmetic is a notorious source of type safety violations.)### Stores

We use store_lookup n st to retrieve the value of the reference
cell at location n in the store st. Note that we must give a
default value to nth in case we try looking up an index which is
too large. (In fact, we will never actually do this, but proving
it will of course require some work!)

To add a new reference cell to the store, we use snoc.

Fixpoint snoc {A:Type} (l:list A) (x:A) : list A :=

match l with

| nil => x :: nil

| h :: t => h :: snoc t x

end.

match l with

| nil => x :: nil

| h :: t => h :: snoc t x

end.

We will need some boring lemmas about snoc. The proofs are
routine inductions.

Lemma length_snoc : forall A (l:list A) x,

length (snoc l x) = S (length l).

Proof.

induction l; intros; [ auto | simpl; rewrite IHl; auto ]. Qed.

Lemma nth_lt_snoc : forall A (l:list A) x d n,

n < length l ->

nth n l d = nth n (snoc l x) d.

Proof.

induction l as [|a l']; intros; try solve by inversion.

Case "l = a :: l'".

destruct n; auto.

simpl. apply IHl'.

simpl in H. apply lt_S_n in H. assumption.

Qed.

Lemma nth_eq_snoc : forall A (l:list A) x d,

nth (length l) (snoc l x) d = x.

Proof.

induction l; intros; [ auto | simpl; rewrite IHl; auto ].

Qed.

To update the store, we use the replace function, which replaces
the contents of a cell at a particular index.

Fixpoint replace {A:Type} (n:nat) (x:A) (l:list A) : list A :=

match l with

| nil => nil

| h :: t =>

match n with

| O => x :: t

| S n' => h :: replace n' x t

end

end.

Of course, we also need some boring lemmas about replace, which
are also fairly straightforward to prove.

Lemma replace_nil : forall A n (x:A),

replace n x [] = [].

Proof.

destruct n; auto.

Qed.

Lemma length_replace : forall A n x (l:list A),

length (replace n x l) = length l.

Proof with auto.

intros A n x l. generalize dependent n.

induction l; intros n.

destruct n...

destruct n...

simpl. rewrite IHl...

Qed.

Lemma lookup_replace_eq : forall l t st,

l < length st ->

store_lookup l (replace l t st) = t.

Proof with auto.

intros l t st.

unfold store_lookup.

generalize dependent l.

induction st as [|t' st']; intros l Hlen.

Case "st = []". inversion Hlen.

Case "st = t' :: st'".

destruct l; simpl...

apply IHst'. simpl in Hlen. omega.

Qed.

Lemma lookup_replace_neq : forall l1 l2 t st,

l1 <> l2 ->

store_lookup l1 (replace l2 t st) = store_lookup l1 st.

Proof with auto.

unfold store_lookup.

induction l1 as [|l1']; intros l2 t st Hneq.

Case "l1 = 0".

destruct st.

SCase "st = []". rewrite replace_nil...

SCase "st = _ :: _". destruct l2... contradict Hneq...

Case "l1 = S l1'".

destruct st as [|t2 st2].

SCase "st = []". destruct l2...

SCase "st = t2 :: st2".

destruct l2...

simpl; apply IHl1'...

Qed.

### Reduction

value v2 | (ST_AppAbs) |

(\a:T.t12) v2 / st --> [v2/a]t12 / st |

t1 / st --> t1' / st' | (ST_App1) |

t1 t2 / st --> t1' t2 / st' |

value v1 t2 / st --> t2' / st' | (ST_App2) |

v1 t2 / st --> v1 t2' / st' |

*programmers*to write terms involving explicit, concrete locations: such terms will arise only as intermediate results of evaluation.

t1 / st --> t1' / st' | (ST_Deref) |

!t1 / st --> !t1' / st' |

l < |st| | (ST_DerefLoc) |

!(loc l) / st --> lookup l st / st |

t1 / st --> t1' / st' | (ST_Assign1) |

t1 := t2 / st --> t1' := t2 / st' |

t2 / st --> t2' / st' | (ST_Assign2) |

t1 := t2 / st --> t1 := t2' / st' |

l < |st| | (ST_Assign) |

loc l := v2 / st --> unit / [v2/l]st |

t1 / st --> t1' / st' | (ST_Ref) |

ref t1 / st --> ref t1' / st' |

(ST_RefValue) | |

ref v1 / st --> loc |st| / st,v1 |

Reserved Notation "t1 '/' st1 '-->' t2 '/' st2"

(at level 40, st1 at level 39, t2 at level 39).

Inductive step : tm * store -> tm * store -> Prop :=

| ST_AppAbs : forall x T t12 v2 st,

value v2 ->

tm_app (tm_abs x T t12) v2 / st --> subst x v2 t12 / st

| ST_App1 : forall t1 t1' t2 st st',

t1 / st --> t1' / st' ->

tm_app t1 t2 / st --> tm_app t1' t2 / st'

| ST_App2 : forall v1 t2 t2' st st',

value v1 ->

t2 / st --> t2' / st' ->

tm_app v1 t2 / st --> tm_app v1 t2'/ st'

| ST_SuccNat : forall n st,

tm_succ (tm_nat n) / st --> tm_nat (S n) / st

| ST_Succ : forall t1 t1' st st',

t1 / st --> t1' / st' ->

tm_succ t1 / st --> tm_succ t1' / st'

| ST_PredNat : forall n st,

tm_pred (tm_nat n) / st --> tm_nat (pred n) / st

| ST_Pred : forall t1 t1' st st',

t1 / st --> t1' / st' ->

tm_pred t1 / st --> tm_pred t1' / st'

| ST_MultNats : forall n1 n2 st,

tm_mult (tm_nat n1) (tm_nat n2) / st --> tm_nat (mult n1 n2) / st

| ST_Mult1 : forall t1 t2 t1' st st',

t1 / st --> t1' / st' ->

tm_mult t1 t2 / st --> tm_mult t1' t2 / st'

| ST_Mult2 : forall v1 t2 t2' st st',

value v1 ->

t2 / st --> t2' / st' ->

tm_mult v1 t2 / st --> tm_mult v1 t2' / st'

| ST_If0 : forall t1 t1' t2 t3 st st',

t1 / st --> t1' / st' ->

tm_if0 t1 t2 t3 / st --> tm_if0 t1' t2 t3 / st'

| ST_If0_Zero : forall t2 t3 st,

tm_if0 (tm_nat 0) t2 t3 / st --> t2 / st

| ST_If0_Nonzero : forall n t2 t3 st,

tm_if0 (tm_nat (S n)) t2 t3 / st --> t3 / st

| ST_RefValue : forall v1 st,

value v1 ->

tm_ref v1 / st --> tm_loc (length st) / snoc st v1

| ST_Ref : forall t1 t1' st st',

t1 / st --> t1' / st' ->

tm_ref t1 / st --> tm_ref t1' / st'

| ST_DerefLoc : forall st l,

l < length st ->

tm_deref (tm_loc l) / st --> store_lookup l st / st

| ST_Deref : forall t1 t1' st st',

t1 / st --> t1' / st' ->

tm_deref t1 / st --> tm_deref t1' / st'

| ST_Assign : forall v2 l st,

value v2 ->

l < length st ->

tm_assign (tm_loc l) v2 / st --> tm_unit / replace l v2 st

| ST_Assign1 : forall t1 t1' t2 st st',

t1 / st --> t1' / st' ->

tm_assign t1 t2 / st --> tm_assign t1' t2 / st'

| ST_Assign2 : forall v1 t2 t2' st st',

value v1 ->

t2 / st --> t2' / st' ->

tm_assign v1 t2 / st --> tm_assign v1 t2' / st'

where "t1 '/' st1 '-->' t2 '/' st2" := (step (t1,st1) (t2,st2)).

Tactic Notation "step_cases" tactic(first) tactic(c) :=

first;

[ c "ST_AppAbs" | c "ST_App1" | c "ST_App2"

| c "ST_SuccNat" | c "ST_Succ" | c "ST_PredNat" | c "ST_Pred"

| c "ST_MultNats" | c "ST_Mult1" | c "ST_Mult2"

| c "ST_If0" | c "ST_If0_Zero" | c "ST_If0_Nonzero"

| c "ST_RefValue"

| c "ST_Ref" | c "ST_DerefLoc" | c "ST_Deref" | c "ST_Assign"

| c "ST_Assign1" | c "ST_Assign2" ].

Hint Constructors step.

Definition stepmany := (refl_step_closure step).

Notation "t1 '/' st '-->*' t2 '/' st'" := (stepmany (t1,st) (t2,st'))

(at level 40, st at level 39, t2 at level 39).

Definition partial_map (A:Type) := id -> option A.

Definition context := partial_map ty.

Definition empty {A:Type} : partial_map A := (fun _ => None).

Definition extend {A:Type} (Gamma : partial_map A) (x:id) (T : A) :=

fun x' => if beq_id x x' then Some T else Gamma x'.

Lemma extend_eq : forall A (ctxt: partial_map A) x T,

(extend ctxt x T) x = Some T.

Proof.

intros. unfold extend. rewrite <- beq_id_refl. auto.

Qed.

Lemma extend_neq : forall A (ctxt: partial_map A) x1 T x2,

beq_id x2 x1 = false ->

(extend ctxt x2 T) x1 = ctxt x1.

Proof.

intros. unfold extend. rewrite H. auto.

Qed.

Lemma extend_shadow : forall A (ctxt: partial_map A) t1 t2 x1 x2,

extend (extend ctxt x2 t1) x2 t2 x1 = extend ctxt x2 t2 x1.

Proof with auto.

intros. unfold extend. destruct (beq_id x2 x1)...

Qed.

### Store typings

Gamma |- lookup l st : T1 | |

Gamma |- loc l : Ref T1 |

*stores*, terms, and types). Since the store is, intuitively, part of the context in which we calculate the type of a term, let's write this four-place relation with the store to the left of the turnstile: Gamma; st |- t : T. Our rule for typing references now has the form

Gamma; st |- lookup l st : T1 | |

Gamma; st |- loc l : Ref T1 |

*their*types each time they appear.

*cycle*. For example, there is no finite typing derivation for the location 0 with respect to this store:

[\x:Nat. (!(loc 1)) x, \x:Nat. (!(loc 0)) x]

#### Exercise: 2 stars

Can you find a term whose evaluation will create this particular cyclic store? ☐*store typing*---a finite function mapping locations to types.

The store_ty_lookup function retrieves the type at a particular
index.

Suppose we are

That is, as long as l is a valid location (it is less than the
length of ST), we can compute the type of l just by looking it
up in ST. Typing is again a four-place relation, but it is
parameterized on a store
We can now give the typing relation for the STLC with references.
The rules for variables, abstraction, and application are the same
as before (with the addition of a store typing which is ignored).

*given*a store typing ST describing the store st in which some term t will be evaluated. Then we can use ST to calculate the type of the result of t without ever looking directly at st. For example, if ST is [Unit, Unit->Unit], then we may immediately infer that !(loc 1) has type Unit->Unit. More generally, the typing rule for locations can be reformulated in terms of store typings like this:l < |ST| | |

Gamma; ST |- loc l : Ref (lookup l st) |

*typing*rather than a concrete store. The rest of the typing rules are analogously augmented with store typings.### The Typing Relation

(T_Unit) | |

Gamma; ST |- unit : Unit |

l < |ST| | (T_Loc) |

Gamma; ST |- loc l : Ref (lookup l st) |

Gamma; ST |- t1 : T1 | (T_Ref) |

Gamma; ST |- ref t1 : Ref T1 |

Gamma; ST |- t1 : Ref T11 | (T_Deref) |

Gamma; ST |- !t1 : T11 |

Gamma; ST |- t1 : Ref T11 | |

Gamma; ST |- t2 : T11 | (T_Assign) |

Gamma; ST |- t1 := t2 : Unit |

Inductive has_type : context -> store_ty -> tm -> ty -> Prop :=

| T_Var : forall Gamma ST x T,

Gamma x = Some T ->

has_type Gamma ST (tm_var x) T

| T_Abs : forall Gamma ST x T11 T12 t12,

has_type (extend Gamma x T11) ST t12 T12 ->

has_type Gamma ST (tm_abs x T11 t12) (ty_arrow T11 T12)

| T_App : forall T1 T2 Gamma ST t1 t2,

has_type Gamma ST t1 (ty_arrow T1 T2) ->

has_type Gamma ST t2 T1 ->

has_type Gamma ST (tm_app t1 t2) T2

| T_Nat : forall Gamma ST n,

has_type Gamma ST (tm_nat n) ty_nat

| T_Succ : forall Gamma ST t1,

has_type Gamma ST t1 ty_nat ->

has_type Gamma ST (tm_succ t1) ty_nat

| T_Pred : forall Gamma ST t1,

has_type Gamma ST t1 ty_nat ->

has_type Gamma ST (tm_pred t1) ty_nat

| T_Mult : forall Gamma ST t1 t2,

has_type Gamma ST t1 ty_nat ->

has_type Gamma ST t2 ty_nat ->

has_type Gamma ST (tm_mult t1 t2) ty_nat

| T_If0 : forall Gamma ST t1 t2 t3 T,

has_type Gamma ST t1 ty_nat ->

has_type Gamma ST t2 T ->

has_type Gamma ST t3 T ->

has_type Gamma ST (tm_if0 t1 t2 t3) T

| T_Unit : forall Gamma ST,

has_type Gamma ST tm_unit ty_unit

| T_Loc : forall Gamma ST l,

l < length ST ->

has_type Gamma ST (tm_loc l) (ty_ref (store_ty_lookup l ST))

| T_Ref : forall Gamma ST t1 T1,

has_type Gamma ST t1 T1 ->

has_type Gamma ST (tm_ref t1) (ty_ref T1)

| T_Deref : forall Gamma ST t1 T11,

has_type Gamma ST t1 (ty_ref T11) ->

has_type Gamma ST (tm_deref t1) T11

| T_Assign : forall Gamma ST t1 t2 T11,

has_type Gamma ST t1 (ty_ref T11) ->

has_type Gamma ST t2 T11 ->

has_type Gamma ST (tm_assign t1 t2) ty_unit.

Hint Constructors has_type.

Tactic Notation "typing_cases" tactic(first) tactic(c) :=

first;

[ c "T_Var" | c "T_Abs" | c "T_App"

| c "T_Nat" | c "T_Succ" | c "T_Pred" | c "T_Mult" | c "T_If0"

| c "T_Unit" | c "T_Loc" | c "T_Ref" | c "T_Deref" | c "T_Assign" ].

Of course, these typing rules will accurately predict the results
of evaluation only if the concrete store used during evaluation
actually conforms to the store typing that we assume for purposes
of typechecking. This proviso exactly parallels the situation
with free variables in the STLC: the substitution lemma promises
us that, if Gamma |- t : T, then we can replace the free
variables in t with values of the types listed in Gamma to
obtain a closed term of type T, which, by the type preservation
theorem will evaluate to a final result of type T if it yields
any result at all. We will see later how to formalize an
analogous intuition for stores and store typings.
Finally, note that, for purposes of typechecking the terms that
programmers actually write, we do not need to do anything tricky
to guess what store typing we should use. Concrete location
constants arise only in terms that are the intermediate results of
evaluation; they are not in the language that programmers write.
Thus, we can simply typecheck the programmer's terms with respect
to the
Our final task is to check that standard type safety properties
continue to hold for the STLC with references. The progress
theorem ("well-typed terms are not stuck") can be stated and
proved almost as for the STLC; we just need to add a few
straightforward cases to the proof, dealing with the new
constructs. The preservation theorem is a bit more interesting,
so let's look at it first.
Since we have extended both the evaluation relation (with initial
and final stores) and the typing relation (with a store typing),
we need to change the statement of preservation to include these
parameters. Clearly, though, we cannot just add stores and store
typings without saying anything about how they are related:

*empty*store typing. As evaluation proceeds and new locations are created, we will always be able to see how to extend the store typing by looking at the type of the initial values being placed in newly allocated cells; this intuition is formalized in the statement of the type preservation theorem below.## Safety

### Well Typed Stores

Theorem preservation_wrong1 : forall ST T t st t' st',

has_type empty ST t T ->

t / st --> t' / st' ->

has_type empty ST t' T.

Abort.

If we typecheck with respect to some set of assumptions about the
types of the values in the store and then evaluate with respect to
a store that violates these assumptions, the result will be
disaster. We say that a store st is

*well typed*with repsect to a typing context Gamma and a store typing ST if the term at each location l in st has the type at location l in ST. The following definition of store_well_typed formalizes this.Definition store_well_typed (Gamma:context) (ST:store_ty) (st:store) :=

length ST = length st /\

(forall l,

l < length st ->

has_type Gamma ST (store_lookup l st) (store_ty_lookup l ST)).

Informally, we will write Gamma; ST |- st for store_well_typed
Gamma ST st.
Intuitively, a store st is consistent with a
store typing ST if every value in the store has the type
predicted by the store typing. (The only subtle point is the fact
that, when typing the values in the store, we supply the very same
store typing to the typing relation!)

#### Exercise: 2 stars

Can you find a context Gamma, a store st, and two different store typings ST1 and ST2 such that both Gamma; ST1 |- st and Gamma; ST2 |- st?
(* FILL IN HERE *)

☐
We can now state something closer to the desired preservation
property:

Theorem preservation_wrong2 : forall ST T t st t' st',

has_type empty ST t T ->

t / st --> t' / st' ->

store_well_typed empty ST st ->

has_type empty ST t' T.

Abort.

This statement is fine for all of the evaluation rules except the
allocation rule ST_RefValue. The problem is that this rule
yields a store with a larger domain than the initial store, which
falsifies the conclusion of the above statement: if ST'
includes a binding for a fresh location l, then l cannot be in
the domain of ST, and it will not be the case that t'
(which definitely mentions l) is typable under ST.
Evidently, since the store can increase in size during evaluation,
we need to allow the store typing to grow as well. This motivates
the following definition. We say that the store type ST'

### Extending Store Typings

*extends*ST if ST' is just ST with some new types added to the end.Inductive extends : store_ty -> store_ty -> Prop :=

| extends_nil : forall ST', extends ST' nil

| extends_cons : forall x ST' ST, extends ST' ST -> extends (x::ST') (x::ST).

Hint Constructors extends.

We'll need a few lemmas about extended contexts. First, looking up
a type in an extended store typing yields the same result as in
the original:

Lemma extends_lookup : forall l ST ST',

l < length ST ->

extends ST' ST ->

store_ty_lookup l ST' = store_ty_lookup l ST.

Proof with auto.

intros l ST ST' Hlen H. generalize dependent ST'. generalize dependent l.

induction ST as [|a ST2]; intros l Hlen ST' HST'.

Case "nil". inversion Hlen.

Case "cons". unfold store_ty_lookup in *.

destruct ST' as [|a' ST'2].

SCase "ST' = nil". inversion HST'.

SCase "ST' = a' :: ST'2".

inversion HST'; subst.

destruct l as [|l'].

SSCase "l = 0"...

SSCase "l = S l'". simpl. apply IHST2...

simpl in Hlen; omega.

Qed.

If ST' extends ST, the length of ST' is at least that of
ST.

Lemma length_extends : forall l ST ST',

l < length ST ->

extends ST' ST ->

l < length ST'.

Proof with eauto.

intros. generalize dependent l. induction H0; intros l Hlen.

inversion Hlen.

simpl in *.

destruct l; try omega.

apply lt_n_S. apply IHextends. omega.

Qed.

Finally, snoc ST T extends ST, and extends is reflexive.

Lemma extends_snoc : forall ST T,

extends (snoc ST T) ST.

Proof with auto.

induction ST; intros T...

simpl...

Qed.

Lemma extends_refl : forall ST,

extends ST ST.

Proof.

induction ST; auto.

Qed.

### Preservation, Finally

Theorem preservation : forall ST t t' T st st',

has_type empty ST t T ->

store_well_typed empty ST st ->

t / st --> t' / st' ->

exists ST',

(extends ST' ST /\

has_type empty ST' t' T /\

store_well_typed empty ST' st').

has_type empty ST t T ->

store_well_typed empty ST st ->

t / st --> t' / st' ->

exists ST',

(extends ST' ST /\

has_type empty ST' t' T /\

store_well_typed empty ST' st').

*some*store typing ST' extending ST (i.e., agreeing with ST on the values of all the old locations) such that the new term t' is well typed with respect to ST'; it does not tell us exactly what ST' is. It is intuitively clear, of course, that ST' is either ST or else it is exactly snoc ST T1, where T1 is the type of the value v1 in the extended store snoc st v1, but stating this explicitly would complicate the statement of the theorem without actually making it any more useful: the weaker version above is already in the right form (because its conclusion implies its hypothesis) to "turn the crank" repeatedly and conclude that every

*sequence*of evaluation steps preserves well-typedness. Combining this with the progress property, we obtain the usual guarantee that "well-typed programs never go wrong."

### Substitution lemma

Inductive appears_free_in : id -> tm -> Prop :=

| afi_var : forall x,

appears_free_in x (tm_var x)

| afi_app1 : forall x t1 t2,

appears_free_in x t1 -> appears_free_in x (tm_app t1 t2)

| afi_app2 : forall x t1 t2,

appears_free_in x t2 -> appears_free_in x (tm_app t1 t2)

| afi_abs : forall x y T11 t12,

y <> x ->

appears_free_in x t12 ->

appears_free_in x (tm_abs y T11 t12)

| afi_succ : forall x t1,

appears_free_in x t1 ->

appears_free_in x (tm_succ t1)

| afi_pred : forall x t1,

appears_free_in x t1 ->

appears_free_in x (tm_pred t1)

| afi_mult1 : forall x t1 t2,

appears_free_in x t1 ->

appears_free_in x (tm_mult t1 t2)

| afi_mult2 : forall x t1 t2,

appears_free_in x t2 ->

appears_free_in x (tm_mult t1 t2)

| afi_if0_1 : forall x t1 t2 t3,

appears_free_in x t1 ->

appears_free_in x (tm_if0 t1 t2 t3)

| afi_if0_2 : forall x t1 t2 t3,

appears_free_in x t2 ->

appears_free_in x (tm_if0 t1 t2 t3)

| afi_if0_3 : forall x t1 t2 t3,

appears_free_in x t3 ->

appears_free_in x (tm_if0 t1 t2 t3)

| afi_ref : forall x t1,

appears_free_in x t1 -> appears_free_in x (tm_ref t1)

| afi_deref : forall x t1,

appears_free_in x t1 -> appears_free_in x (tm_deref t1)

| afi_assign1 : forall x t1 t2,

appears_free_in x t1 -> appears_free_in x (tm_assign t1 t2)

| afi_assign2 : forall x t1 t2,

appears_free_in x t2 -> appears_free_in x (tm_assign t1 t2).

Tactic Notation "afi_cases" tactic(first) tactic(c) :=

first;

[ c "afi_var" | c "afi_app1" | c "afi_app2" | c "afi_abs"

| c "afi_succ" | c "afi_pred" | c "afi_mult1" | c "afi_mult2"

| c "afi_if0_1" | c "afi_if0_2" | c "afi_if0_3"

| c "afi_ref" | c "afi_deref" | c "afi_assign1" | c "afi_assign2" ].

Hint Constructors appears_free_in.

Lemma free_in_context : forall x t T Gamma ST,

appears_free_in x t ->

has_type Gamma ST t T ->

exists T', Gamma x = Some T'.

Proof with eauto.

intros. generalize dependent Gamma. generalize dependent T.

(afi_cases (induction H) Case); intros; (try solve [ inversion H0; subst; eauto ]).

Case "afi_abs".

inversion H1; subst.

apply IHappears_free_in in H8.

apply not_eq_beq_id_false in H.

rewrite extend_neq in H8; assumption.

Qed.

Lemma context_invariance : forall Gamma Gamma' ST t T,

has_type Gamma ST t T ->

(forall x, appears_free_in x t -> Gamma x = Gamma' x) ->

has_type Gamma' ST t T.

Proof with eauto.

intros.

generalize dependent Gamma'.

(typing_cases (induction H) Case); intros...

Case "T_Var".

apply T_Var. symmetry. rewrite <- H...

Case "T_Abs".

apply T_Abs. apply IHhas_type; intros.

unfold extend.

remember (beq_id x x0) as e; destruct e...

apply H0. apply afi_abs. apply beq_id_false_not_eq... auto.

Case "T_App".

eapply T_App.

apply IHhas_type1...

apply IHhas_type2...

Case "T_Mult".

eapply T_Mult.

apply IHhas_type1...

apply IHhas_type2...

Case "T_If0".

eapply T_If0.

apply IHhas_type1...

apply IHhas_type2...

apply IHhas_type3...

Case "T_Assign".

eapply T_Assign.

apply IHhas_type1...

apply IHhas_type2...

Qed.

Lemma substitution_preserves_typing : forall Gamma ST x s S t T,

has_type empty ST s S ->

has_type (extend Gamma x S) ST t T ->

has_type Gamma ST (subst x s t) T.

Proof with eauto.

intros Gamma ST x s S t T Hs Ht.

generalize dependent Gamma. generalize dependent T.

(tm_cases (induction t) Case); intros T Gamma H;

inversion H; subst; simpl...

Case "tm_var".

rename i into y.

remember (beq_id x y) as eq; destruct eq; subst.

SCase "x = y".

apply beq_id_eq in Heqeq; subst.

rewrite extend_eq in H3.

inversion H3; subst.

eapply context_invariance...

intros x Hcontra.

destruct (free_in_context _ _ _ _ _ Hcontra Hs) as [T' HT'].

inversion HT'.

SCase "x <> y".

apply T_Var.

rewrite extend_neq in H3...

Case "tm_abs". subst.

rename i into y.

remember (beq_id x y) as eq; destruct eq.

SCase "x = y".

apply beq_id_eq in Heqeq; subst.

apply T_Abs. eapply context_invariance...

intros. apply extend_shadow.

SCase "x <> x0".

apply T_Abs. apply IHt.

eapply context_invariance...

intros. unfold extend.

remember (beq_id y x0) as e. destruct e...

apply beq_id_eq in Heqe; subst.

rewrite <- Heqeq...

Qed.

### Assignment Preserves Store Typing

Lemma assign_pres_store_typing : forall Gamma ST st l t,

l < length st ->

store_well_typed Gamma ST st ->

has_type Gamma ST t (store_ty_lookup l ST) ->

store_well_typed Gamma ST (replace l t st).

Proof with auto.

intros Gamma ST st l t Hlen HST Ht.

inversion HST; subst.

split. rewrite length_replace...

intros l' Hl'.

remember (beq_nat l' l) as ll'; destruct ll'.

Case "l' = l".

apply beq_nat_eq in Heqll'; subst.

rewrite lookup_replace_eq...

Case "l' <> l".

symmetry in Heqll'; apply beq_nat_false in Heqll'.

rewrite lookup_replace_neq...

rewrite length_replace in Hl'.

apply H0...

Qed.

### Weakening for Stores

Lemma store_weakening : forall Gamma ST ST' t T,

extends ST' ST ->

has_type Gamma ST t T ->

has_type Gamma ST' t T.

Proof with eauto.

intros. (typing_cases (induction H0) Case); eauto.

Case "T_Loc".

erewrite <- extends_lookup...

apply T_Loc.

eapply length_extends...

Qed.

We can also use the weakening lemma for stores to prove that if a
store is well-typed with respect to a store typing, then the store
extended with a new term t will still be well-typed with respect
to the store typing extended with t's type.

Lemma store_well_typed_snoc : forall Gamma ST st t1 T1,

store_well_typed Gamma ST st ->

has_type Gamma ST t1 T1 ->

store_well_typed Gamma (snoc ST T1) (snoc st t1).

Proof with auto.

intros.

unfold store_well_typed in *.

inversion H as [Hlen Hmatch]; clear H.

rewrite !length_snoc.

split...

Case "types match.".

intros l Hl.

unfold store_lookup, store_ty_lookup.

apply le_lt_eq_dec in Hl; destruct Hl as [Hlt | Heq].

SCase "l < length st".

apply lt_S_n in Hlt.

rewrite <- !nth_lt_snoc...

apply store_weakening with ST. apply extends_snoc.

apply Hmatch...

rewrite Hlen...

SCase "l = length st".

inversion Heq.

rewrite nth_eq_snoc.

rewrite <- Hlen. rewrite nth_eq_snoc...

apply store_weakening with ST... apply extends_snoc.

Qed.

### Preservation!

Theorem preservation : forall ST t t' T st st',

has_type empty ST t T ->

store_well_typed empty ST st ->

t / st --> t' / st' ->

exists ST',

(extends ST' ST /\

has_type empty ST' t' T /\

store_well_typed empty ST' st').

Proof with eauto using store_weakening, extends_refl.

remember (@empty ty) as Gamma.

intros ST t t' T st st' Ht.

generalize dependent t'.

(typing_cases (induction Ht) Case); intros t' HST Hstep;

subst; try (solve by inversion); inversion Hstep; subst;

try (eauto using store_weakening, extends_refl).

Case "T_App".

SCase "ST_AppAbs". exists ST.

inversion Ht1; subst.

split; try split... eapply substitution_preserves_typing...

SCase "ST_App1".

eapply IHHt1 in H0...

inversion H0 as [ST' [Hext [Hty Hsty]]].

exists ST'...

SCase "ST_App2".

eapply IHHt2 in H5...

inversion H5 as [ST' [Hext [Hty Hsty]]].

exists ST'...

Case "T_Succ".

SCase "ST_Succ".

eapply IHHt in H0...

inversion H0 as [ST' [Hext [Hty Hsty]]].

exists ST'...

Case "T_Pred".

SCase "ST_Pred".

eapply IHHt in H0...

inversion H0 as [ST' [Hext [Hty Hsty]]].

exists ST'...

Case "T_Mult".

SCase "ST_Mult1".

eapply IHHt1 in H0...

inversion H0 as [ST' [Hext [Hty Hsty]]].

exists ST'...

SCase "ST_Mult2".

eapply IHHt2 in H5...

inversion H5 as [ST' [Hext [Hty Hsty]]].

exists ST'...

Case "T_If0".

SCase "ST_If0_1".

eapply IHHt1 in H0...

inversion H0 as [ST' [Hext [Hty Hsty]]].

exists ST'... split...

Case "T_Ref".

SCase "ST_RefValue".

exists (snoc ST T1).

inversion HST; subst.

split.

apply extends_snoc.

split.

replace (ty_ref T1) with (ty_ref (store_ty_lookup (length st) (snoc ST T1))).

apply T_Loc.

rewrite <- H. rewrite length_snoc. omega.

unfold store_ty_lookup. rewrite <- H. rewrite nth_eq_snoc...

apply store_well_typed_snoc; assumption.

SCase "ST_Ref".

eapply IHHt in H0...

inversion H0 as [ST' [Hext [Hty Hsty]]].

exists ST'...

Case "T_Deref".

SCase "ST_DerefLoc".

exists ST. split; try split...

destruct HST as [_ Hsty].

replace T11 with (store_ty_lookup l ST).

apply Hsty...

inversion Ht; subst...

SCase "ST_Deref".

eapply IHHt in H0...

inversion H0 as [ST' [Hext [Hty Hsty]]].

exists ST'...

Case "T_Assign".

SCase "ST_Assign".

exists ST. split; try split...

eapply assign_pres_store_typing...

inversion Ht1; subst...

SCase "ST_Assign1".

eapply IHHt1 in H0...

inversion H0 as [ST' [Hext [Hty Hsty]]].

exists ST'...

SCase "ST_Assign2".

eapply IHHt2 in H5...

inversion H5 as [ST' [Hext [Hty Hsty]]].

exists ST'...

Qed.

### Progress

Theorem progress : forall ST t T st,

has_type empty ST t T ->

store_well_typed empty ST st ->

(value t \/ exists t', exists st', t / st --> t' / st').

Proof with eauto.

intros ST t T st Ht HST. remember (@empty ty) as Gamma.

(typing_cases (induction Ht) Case); subst; try solve by inversion...

Case "T_App".

right. destruct IHHt1 as [Ht1p | Ht1p]...

SCase "t1 is a value".

inversion Ht1p; subst; try solve by inversion.

destruct IHHt2 as [Ht2p | Ht2p]...

SSCase "t2 steps".

inversion Ht2p as [t2' [st' Hstep]].

exists (tm_app (tm_abs x T t) t2'). exists st'...

SCase "t1 steps".

inversion Ht1p as [t1' [st' Hstep]].

exists (tm_app t1' t2). exists st'...

Case "T_Succ".

right. destruct IHHt as [Ht1p | Ht1p]...

SCase "t1 is a value".

inversion Ht1p; subst; try solve [ inversion Ht ].

SSCase "t1 is a tm_nat".

exists (tm_nat (S n)). exists st...

SCase "t1 steps".

inversion Ht1p as [t1' [st' Hstep]].

exists (tm_succ t1'). exists st'...

Case "T_Pred".

right. destruct IHHt as [Ht1p | Ht1p]...

SCase "t1 is a value".

inversion Ht1p; subst; try solve [inversion Ht ].

SSCase "t1 is a tm_nat".

exists (tm_nat (pred n)). exists st...

SCase "t1 steps".

inversion Ht1p as [t1' [st' Hstep]].

exists (tm_pred t1'). exists st'...

Case "T_Mult".

right. destruct IHHt1 as [Ht1p | Ht1p]...

SCase "t1 is a value".

inversion Ht1p; subst; try solve [inversion Ht1].

destruct IHHt2 as [Ht2p | Ht2p]...

SSCase "t2 is a value".

inversion Ht2p; subst; try solve [inversion Ht2].

exists (tm_nat (mult n n0)). exists st...

SSCase "t2 steps".

inversion Ht2p as [t2' [st' Hstep]].

exists (tm_mult (tm_nat n) t2'). exists st'...

SCase "t1 steps".

inversion Ht1p as [t1' [st' Hstep]].

exists (tm_mult t1' t2). exists st'...

Case "T_If0".

right. destruct IHHt1 as [Ht1p | Ht1p]...

SCase "t1 is a value".

inversion Ht1p; subst; try solve [inversion Ht1].

destruct n.

SSCase "n = 0". exists t2. exists st...

SSCase "n = S n'". exists t3. exists st...

SCase "t1 steps".

inversion Ht1p as [t1' [st' Hstep]].

exists (tm_if0 t1' t2 t3). exists st'...

Case "T_Ref".

right. destruct IHHt as [Ht1p | Ht1p]...

SCase "t1 steps".

inversion Ht1p as [t1' [st' Hstep]].

exists (tm_ref t1'). exists st'...

Case "T_Deref".

right. destruct IHHt as [Ht1p | Ht1p]...

SCase "t1 is a value".

inversion Ht1p; subst; try solve by inversion.

eexists. eexists. apply ST_DerefLoc...

inversion Ht; subst. inversion HST; subst.

rewrite <- H...

SCase "t1 steps".

inversion Ht1p as [t1' [st' Hstep]].

exists (tm_deref t1'). exists st'...

Case "T_Assign".

right. destruct IHHt1 as [Ht1p|Ht1p]...

SCase "t1 is a value".

destruct IHHt2 as [Ht2p|Ht2p]...

SSCase "t2 is a value".

inversion Ht1p; subst; try solve by inversion.

eexists. eexists. apply ST_Assign...

inversion HST; subst. inversion Ht1; subst.

rewrite H in H5...

SSCase "t2 steps".

inversion Ht2p as [t2' [st' Hstep]].

exists (tm_assign t1 t2'). exists st'...

SCase "t1 steps".

inversion Ht1p as [t1' [st' Hstep]].

exists (tm_assign t1' t2). exists st'...

Qed.

# References and Nontermination

*normalizing*, that is, every well-typed term can be reduced to a value in a finite number of steps. What about STLC + references? Surprisingly, adding references causes us to lose the normalization property: there exist well-typed terms in the STLC + references which can continue to reduce forever, without ever reaching a normal form!

(\r:Ref (Unit -> Unit). r := (\x:Unit.(!r) unit); (!r) unit) (ref (\x:Unit.unit))

Definition loop_fun :=

tm_abs _x ty_unit (tm_app (tm_deref (tm_var _r)) tm_unit).

Definition loop :=

tm_app

(tm_abs _r (ty_ref (ty_arrow ty_unit ty_unit))

(tm_seq (tm_assign (tm_var _r) loop_fun)

(tm_app (tm_deref (tm_var _r)) tm_unit)))

(tm_ref (tm_abs _x ty_unit tm_unit)).

This term is well-typed:

Lemma loop_typeable : exists T, has_type empty [] loop T.

Proof with eauto.

eexists. unfold loop. unfold loop_fun.

eapply T_App...

eapply T_Abs...

eapply T_App...

eapply T_Abs. eapply T_App. eapply T_Deref. eapply T_Var.

unfold extend. simpl. reflexivity. auto.

eapply T_Assign.

eapply T_Var. unfold extend. simpl. reflexivity.

eapply T_Abs.

eapply T_App...

eapply T_Deref. eapply T_Var. reflexivity.

Qed.

To show formally that the term diverges, we first define the
step_closure of the single-step reduction relation, written
-->+. This is just like the reflexive step closure of
single-step reduction (which we're been writing -->*), except
that it is not reflexive: t -->+ t' means that t can reach
t' by

*one or more*steps of reduction.Inductive step_closure {X:Type} (R: relation X) : X -> X -> Prop :=

| sc_one : forall (x y : X),

R x y -> step_closure R x y

| sc_step : forall (x y z : X),

R x y ->

step_closure R y z ->

step_closure R x z.

Definition stepmany1 := (step_closure step).

Notation "t1 '/' st '-->+' t2 '/' st'" := (stepmany1 (t1,st) (t2,st'))

(at level 40, st at level 39, t2 at level 39).

Now, we can show that the expression loop reduces to the
expression !(loc 0) unit and the size-one store [(loc 0) / r]
loop_fun.

Lemma loop_steps_to_loop_fun :

loop / [] -->*

tm_app (tm_deref (tm_loc 0)) tm_unit / [subst _r (tm_loc 0) loop_fun].

Proof with eauto.

unfold loop.

eapply rsc_step. apply ST_App2...

eapply rsc_step. simpl. apply ST_AppAbs...

eapply rsc_step; simpl. apply ST_App2...

eapply rsc_step. apply ST_AppAbs...

eapply rsc_step; simpl. apply ST_App1...

eapply rsc_step; compute. apply ST_AppAbs...

simpl. apply rsc_refl.

Qed.

Finally, the latter expression reduces in two steps to itself!

Lemma loop_fun_step_self :

tm_app (tm_deref (tm_loc 0)) tm_unit / [subst _r (tm_loc 0) loop_fun] -->+

tm_app (tm_deref (tm_loc 0)) tm_unit / [subst _r (tm_loc 0) loop_fun].

Proof with eauto.

unfold loop_fun; simpl.

eapply sc_step. apply ST_App1...

eapply sc_one. compute. apply ST_AppAbs...

Qed.

#### Exercise: 4 stars

Use the above ideas to implement a factorial function in STLC with references. (There is no need to prove formally that it really behaves like the factorial. Just use the example below to make sure it gives the correct result when applied to the argument 4.)Definition factorial : tm :=

(* FILL IN HERE *) admit.

Lemma factorial_type : has_type empty [] factorial (ty_arrow ty_nat ty_nat).

Proof with eauto.

(* FILL IN HERE *) Admitted.

If your definition is correct, you should be able to just
uncomment the example below; the proof should be fully
automatic using the following tactic.

Ltac print_goal := match goal with |- ?x => idtac x end.

Ltac normalize :=

repeat (print_goal; eapply rsc_step ;

[ (eauto 10; fail) | (instantiate; compute)]);

apply rsc_refl.

Ltac normalize :=

repeat (print_goal; eapply rsc_step ;

[ (eauto 10; fail) | (instantiate; compute)]);

apply rsc_refl.

Lemma factorial_4 : exists st, tm_app factorial (tm_nat 4) / [] -->* tm_nat 24 / st. Proof. eexists. unfold factorial. normalize. Qed.☐