## Assignment #6: References

This assignment has 15 points.

1.  [2 points]  Write a well-typed, non-terminating program in a typed lambda calculus that only has unit, non-recursive functions (ie:  \x:t.e) and references (ie: operations ref e, e1 := e2 and !e).

2.  [6 points]  Prove the type preservation lemma for a language with unit, non-recursive functions and references.  In other words, prove that:

If |- (M,e) : t and (M,e) --> (M', e') then (M', e') : t

The syntax of types and expressions are:

t ::= unit | t1 -> t2 | t ref

e ::= x | () | e1; e2 | \x:t.e | e1 e2 | ref e | e1 := e2 | !e | l

v ::= () | \x:t.e | l

M ::= . | M,l -> v          (treat as a function from locations l to values v)

Psi ::= . | Psi, l:t            (treat as a function from locations l to types t)

You may assume the following lemmas have already been proven:

Lemma 1:  If |- M : Psi and l not in Dom(M) and Psi; . |- v : t then |- (M,l->v) : (Psi,l:t)

Lemma 2:  If |- M : Psi and Psi(l) = t and Psi; . |- v : t then |- M[l->v] : Psi

Lemma 3:  If |- M : Psi and l in Dom(M) then Psi; . |- M(l) : Psi(l)

Lemma 4:  If Psi;G |- e : t and l not in Dom(Psi) then Psi,l:t';G |- e : t

Only do the proof for the three cases involving these operational rules:

(l not in Dom(M))

--------------------------- (E-ref)

(M;ref v)  --> (M,l-> v; l)

(l in Dom(M))

------------------------------- (E-assign)

(M; l := v) --> (M[l -> v]; ())

(l in Dom(M))

------------------------------- (E-deref)

(M; !l ) --> (M; M(l))

3.  [7 points]  Implement the operational semantics of (ie: an interpreter for) a language that only has references and unit in SML.  The expressions of your language should be:

e ::= v | e1; e2 | ref e | e1 := e2 | !e

v ::= () | l

M ::= . | M,l -> v

You should define the syntax of expressions using a datatype. You may implement locations using integers. eg:

datatype val =

Unit

| Loc of int

datatype exp =

Val of val

| Seq of exp * exp           (* this is semicolon *)

| ...

You should also define a type for memories:

type memory = ...

Your main job will be to define:

• a function eval that implements a single step of the operational semantics

• a function printval that prints out a value legibly (print out a location by printing the integer that represents it; print the unit value as ())

• a function printmemory that prints out a memory in a legible way (eg, as a list of location, value pairs)

• a function evalstar that executes as many steps of the operational semantics as possible (ie: until a value is reached) and prints out the final value and the final memory at the end

The evaluation functions may assume that all expressions and memories are well-typed.  You may raise the exception Bad if you run in to a situation you

cannot implement (because, for instance, a memory reference is out of bounds):