Mutable state

This article presents a simple language with mutable state—it has let-statements but, unlike many other examples such as the simply-typed lambda calculus, it does not have functions, though this is for simplicity and is not an inherent limitation. It is based on Chapter 2 of Rob Simmons’s undergraduate thesis, which contains more commentary—this account includes a simple extension, the ability to update state. That account is in turn based on Pierce’s description in TAPL. This example can be seen as an extension of the one from the tutorial on strengthening; that example defines a language with references but no way to use them.

Language definition

Natural numbers

First we need natural numbers, which we will use in the object language to represent both locations and actual numbers (this is why we define sum as well.)

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort sum {_ nat} {_ nat} {_ nat} %.
%mode sum %in %in %out %.
%term sum-z sum z N N %.
%term sum-s %pi (sum (s N1) N2 (s N3)) %<- (sum N1 N2 N3) %.
%worlds () (sum A B C) %.
%total A (sum A B C) %.

Syntax

Using this we can define the syntax of the language; natural numbers will be used both for locations (which the programmer cannot access) and as numbers, which can be added—the typing rules will ensure that natural numbers representing heap locations cannot be confused with natural numbers that may be added.

• n N - integrates natural numbers into the language as $\mathsf{n}(n)$, where $\texttt{}n$ is a natural number 0, 1, 2…
• E1 + E2 - addition, $\texttt{}e_1 + e_2$
• ref E - creating a reference cell, $\mathsf{ref}(e)$
• ! E - dereferencing a reference cell, $\texttt{}!e$
• gets E1 E2 - updating a reference cell, $\texttt{}e_1 := e_2$
• loc L - locations (not available to the programmer), $\mathsf{loc}(l)$, where $\texttt{}l$ is an abstract location.
• let E1 ([x] E2 x) - let statements $\mathsf{let~} x = e_1 \mathsf{~in~} e_2$

%inline location nat %.
%sort exp %.
%term n %pi nat %-> exp %.
%term + %pi exp %-> exp %-> exp %.
%prec %left 10 + %.
%term ref %pi exp %-> exp %.
%term ! %pi exp %-> exp %.
%term gets %pi exp %-> exp %-> exp %.
%term loc %pi location %-> exp %.
%term let %pi exp %-> (%pi exp %-> exp) %-> exp %.

Types

Because we do not have functions, our language has a very simple language of types, only integers and references to other types.

%sort tp %.
%term int-tp tp %.
%term ref-tp %pi tp %-> tp %.

Lists

We will represent the store as a list of expressions, and define several operations on lists—projecting the _n_th element from a list, appending a new element to the end of a list, updating the _n_th element of the list, and having a list that is the subset of another list. We also define a similar list of types that is omitted.

%sort explist %.
%term $exp %pi exp %-> explist %-> explist %.
%prec %right 5 $exp %.
%term nil-exp explist %.
%sort proj-exp {_ explist} {_ nat} {_ exp} %.
%mode proj-exp %in %in %out %.
%term proj-exp-z proj-exp (E $exp EL) z E %.
%term proj-exp-s %pi (proj-exp (E $exp EL) (s N) E’) %<- (proj-exp EL N E’) %.
%sort append-exp {_ explist} {_ exp} {_ explist} {_ nat} %.
%mode append-exp %in %in %out %out %.
%term append-exp-z append-exp nil-exp E (E $exp nil-exp) z %.
%term append-exp-s %pi (append-exp (E’ $exp EL) E (E’ $exp EL’) (s N)) %<- (append-exp EL E EL’ N) %.
%sort subset-exp {_ explist} {_ explist} %.
%mode subset-exp %in %in %.
%term subset-exp-z subset-exp nil-exp E %.
%term subset-exp-s %pi (subset-exp (E $exp EL) (E $exp EL’)) %<- (subset-exp EL EL’) %.
%sort update-exp {_ explist} {_ nat} {_ exp} {_ explist} %.
%mode update-exp %in %in %in %out %.
%term update-exp-z update-exp (E $exp EL) z E' (E' $exp EL) %.
%term update-exp-s %pi (update-exp (E $exp EL) (s N) E' (E $exp EL')) %<- (update-exp EL N E' EL') %.
%sort tplist %.
%term $tp %pi tp %-> tplist %-> tplist %.
%prec %right 5 $tp %.
%term nil-tp tplist %.
%sort proj-tp {_ tplist} {_ nat} {_ tp} %.
%mode proj-tp %in %in %out %.
%term proj-tp-z proj-tp (T $tp TL) z T %.
%term proj-tp-s %pi (proj-tp (T $tp TL) (s N) T’) %<- (proj-tp TL N T’) %.
%sort append-tp {_ tplist} {_ tp} {_ tplist} {_ nat} %.
%mode append-tp %in %in %out %out %.
%term append-tp-z append-tp nil-tp T (T $tp nil-tp) z %.
%term append-tp-s %pi (append-tp (T’ $tp TL) T (T’ $tp TL’) (s N)) %<- (append-tp TL T TL’ N) %.
%sort subset-tp {_ tplist} {_ tplist} %.
%term subset-tp-z subset-tp nil-tp T %.
%term subset-tp-s %pi (subset-tp (T $tp TL) (T $tp TL’)) %<- (subset-tp TL TL’) %.
%sort update-tp {_ tplist} {_ nat} {_ tp} {_ tplist} %.
%mode update-tp %in %in %in %out %.
%term update-tp-z update-tp (T $tp TL) z T' (T' $tp TL) %.
%term update-tp-s %pi (update-tp (T $tp TL) (s N) T' (T $tp TL')) %<- (update-tp TL N T' TL') %.

We create abbreviations to indicate that we are using expression lists to represent stores and type lists to represent store typings.

%inline store explist %.
%inline storetp tplist %.

Values and evaluation

The predicate isval

%sort isval {_ exp} %.
%mode isval %in %.
%term v-int isval (n N) %.
%term v-loc isval (loc L) %.
%sort isval-list {_ explist} %.
%mode isval-list %in %.
%term vl-z isval-list nil-exp %.
%term vl-s %pi (isval-list (E $exp EL)) %<- (isval E) %<- (isval-list EL) %.
%sort eval {_ store} {_ exp} {_ store} {_ exp} %.
%mode eval %in %in %out %out %.
%term s1-add %pi (eval S (E1 + E2) S’ (E1’ + E2)) %<- (eval S E1 S’ E1’) %.
%term s2-add %pi (eval S (E1 + E2) S’ (E1 + E2’)) %<- (isval E1) %<- (eval S E2 S’ E2’) %.
%term e-add %pi (eval S (n N1 + n N2) S (n N3)) %<- (sum N1 N2 N3) %.
%term s-ref %pi (eval S (ref E) S’ (ref E’)) %<- (eval S E S’ E’) %.
%term e-ref %pi (eval S (ref E) S’ (loc L)) %<- (isval E) %<- (append-exp S E S’ L) %.
%term s-bang %pi (eval S (! E) S’ (! E’)) %<- (eval S E S’ E’) %.
%term e-bang %pi (eval S (! (loc L)) S E) %<- (proj-exp S L E) %.
%term s1-gets %pi (eval S (gets E1 E2) S' (gets E1' E2)) %<- (eval S E1 S' E1') %.
%term s2-gets %pi (eval S (gets E1 E2) S' (gets E1 E2')) %<- (isval E1) %<- (eval S E2 S' E2') %.
%term e-gets %pi (eval S (gets (loc L1) E) S' E) %<- (isval E) %<- (update-exp S L1 E S') %.
%term s-let %pi (eval S (let E EF) S’ (let E’ EF)) %<- (eval S E S’ E’) %.
%term e-let %pi (eval S (let E EF) S (EF E)) %<- (isval E) %.

Typing judgment

As we do in the article on strengthening, we need to define a separate judgment var-of that we will use to represent hypothetical typing judgments—the hypothetical judgment simply associates an expression with a type, whereas the typing judgment of associates an expression with a type in a specific store typing.

%sort var-of {_ exp} {_ tp} %.
%mode var-of %in %out %.
%sort of {_ storetp} {_ exp} {_ tp} %.
%mode of %in %in %out %.
%sort of-list {_ storetp} {_ explist} {_ tplist} %.
%mode of-list %in %in %out %.
%term tl-z of-list ST nil-exp nil-tp %.
%term tl-s %pi (of-list ST (E $exp EL) (T $tp TL)) %<- (of ST E T) %<- (of-list ST EL TL) %.
%term t-int of ST (n N) int-tp %.
%term t-add %pi (of ST (E1 + E2) int-tp) %<- (of ST E1 int-tp) %<- (of ST E2 int-tp) %.
%term t-ref %pi (of ST (ref E) (ref-tp T)) %<- (of ST E T) %.
%term t-bang %pi (of ST (! E) T) %<- (of ST E (ref-tp T)) %.
%term t-gets %pi (of ST (gets E1 E2) T) %<- (of ST E1 (ref-tp T)) %<- (of ST E2 T) %.
%term t-loc %pi (of ST (loc L) (ref-tp T)) %<- (proj-tp ST L T) %.
%term t-let
  %pi (of ST (let E EF) T)
  %<- (of ST E T’)
  %<- ({x} %pi (var-of x T’) %-> (of ST (EF x) T)) %.
%term t-var %pi (of ST E T) %<- (var-of E T) %.

The typing judgment exists in an LF context where new expression variables can be introduced if they are related with var-of to a well-formed type. This requirement is expressed by the block var-tp.

%block var-tp [T tp] {x exp} {v var-of x T}%.

We also define a judgment of-store, that expresses a store being well-typed and containing only values.

%sort of-store {_ storetp} {_ store} %.
%term &of-store %pi (of-store TL EL) %<- (isval-list EL) %<- (of-list TL EL TL) %.

Multi-step evaluation

%sort run {_ store} {_ exp} {_ store} {_ exp} %.
%mode run %in %in %out %out %.
%term run-step %pi (run S E S’’ E’’) %<- (eval S E S’ E’) %<- (run S’ E’ S’’ E’’) %.
%term run-end run S E S E %.

Language theory

Effectiveness lemmas

We need a few effectiveness lemmas that show that the sum and append judgments are always derivable.

The can-update theorem is slightly different, establishing that if a particular store has a particular type, then any index that has a corresponding type can be updated.

%sort can-sum {A nat} {B nat} {_ sum A B C} %.
%mode can-sum %in %in %out %.
%term & can-sum z N sum-z %.
%term & %pi (can-sum (s N1) N2 (sum-s SUM)) %<- (can-sum N1 N2 SUM) %.
%worlds () (can-sum _ _ _) %.
%total T (can-sum T _ _) %.
%sort can-append-exp {EL explist} {E exp} {_ append-exp EL E EL' N} %.
%mode can-append-exp %in %in %out %.
%term & can-append-exp nil-exp E append-exp-z %.
%term &
  %pi (can-append-exp (E $exp EL) E' (append-exp-s APPEND))
  %<- (can-append-exp EL E' APPEND) %.
%worlds () (can-append-exp _ _ _) %.
%total T (can-append-exp T _ _) %.

Other auxillary lemmas

%sort of-projection {_ of-list ST EL TL} {_ proj-tp TL N T} {_ proj-exp EL N E} {_ of ST E T} %.
%mode of-projection %in %in %out %out %.
%term & of-projection (tl-s TL T) proj-tp-z proj-exp-z T %.
%term &
  %pi (of-projection (tl-s TL T’) (proj-tp-s PT) (proj-exp-s PE) T)
  %<- (of-projection TL PT PE T) %.
%worlds () (of-projection _ _ _ _) %.
%total PT (of-projection _ PT _ _) %.
%sort of-projection' {_ of-list ST EL TL} {_ proj-tp TL N T} {_ proj-exp EL N E} {_ of ST E T} %.
%mode of-projection' %in %in %in %out %.
%term & of-projection' (tl-s TL T) proj-tp-z proj-exp-z T %.
%term &
  %pi (of-projection' (tl-s TL T’) (proj-tp-s PT) (proj-exp-s PE) T)
  %<- (of-projection' TL PT PE T) %.
%worlds () (of-projection' _ _ _ _) %.
%total PT (of-projection' _ PT _ _) %.
%sort subset-projectable {_ proj-tp ST N T} {_ subset-tp ST ST’} {_ proj-tp ST’ N T} %.
%mode subset-projectable %in %in %out %.
%term & subset-projectable proj-tp-z (subset-tp-s SUB) proj-tp-z %.
%term &
  %pi (subset-projectable (proj-tp-s P) (subset-tp-s SUB) (proj-tp-s P’))
  %<- (subset-projectable P SUB P’) %.
%worlds () (subset-projectable _ _ _) %.
%total P (subset-projectable P S P’) %.
%sort subset-refl {ST} {_ subset-tp ST ST} %.
%mode subset-refl %in %out %.
%term & subset-refl nil-tp subset-tp-z %.
%term & %pi (subset-refl (T $tp ST) (subset-tp-s SUB)) %<- (subset-refl ST SUB) %.
%worlds () (subset-refl _ _) %.
%total T (subset-refl T _) %.
%sort of-update {_ of-list ST EL TL} {_ proj-tp TL L T} {E} {_ update-exp EL L E EL'} %.
%mode of-update %in %in %in %out %.
%term & of-update (tl-s _ _) proj-tp-z _ update-exp-z %.
%term &
  %pi (of-update (tl-s T _) (proj-tp-s PT) E (update-exp-s PE))
  %<- (of-update T PT E PE) %.
%worlds () (of-update _ _ _ _) %.
%total T (of-update T _ _ _) %.
%sort append-lemma {_ isval E} {_ of ST E T} {_ isval-list EL} {_ of-list ST EL TL} {_ append-exp EL E EL’ N} {_ subset-tp TL TL’} {_ isval-list EL’} {_ of-list ST EL’ TL’} {_ proj-tp TL’ N T} %.
%mode append-lemma %in %in %in %in %in %out %out %out %out %.
%term & append-lemma V T vl-z tl-z append-exp-z subset-tp-z (vl-s vl-z V) (tl-s tl-z T) proj-tp-z %.
%term &
  %pi (append-lemma V T (vl-s VL V*) (tl-s TL T*) (append-exp-s AE) (subset-tp-s S) (vl-s VL’ V*) (tl-s TL’ T*) (proj-tp-s P))
  %<- (append-lemma V T VL TL AE S VL’ TL’ P) %.
%worlds () (append-lemma _ _ _ _ _ _ _ _ _) %.
%total [VL TL AE] (append-lemma V T VL TL AE AT VL’ TL’ P) %.
%sort update-lemma {_ isval E} {_ of ST E T} {_ isval-list EL} {_ of-list ST EL TL} {_ proj-tp TL N T} {_ update-exp EL N E EL'} {_ isval-list EL'} {_ of-list ST EL' TL} %.
%mode update-lemma %in %in %in %in %in %in %out %out %.
%term & update-lemma V T (vl-s VL V*) (tl-s TL T*) proj-tp-z update-exp-z (vl-s VL V) (tl-s TL T) %.
%term &
  %pi (update-lemma V T (vl-s VL V*) (tl-s TL T*) (proj-tp-s P) (update-exp-s UE) (vl-s VL' V*) (tl-s TL' T*))
  %<- (update-lemma V T VL TL P UE VL' TL') %.
%worlds () (update-lemma _ _ _ _ _ _ _ _) %.
%total T (update-lemma _ _ T _ _ _ _ _) %.

Progress

Progress, as usual, relies on an auxillary notion of what it means for an expression to not be stuck that is captured by the judgement notstuck, which states that in a certain store S an expression E is either a value or can take a step.

%sort notstuck {_ store} {_ exp} %.
%term ns-steps %pi (notstuck S E) %<- (eval S E S’ E’) %.
%term ns-isval %pi (notstuck S E) %<- (isval E) %.

The statement of the progress theorem then utilizes the progress theorem in a straightforward manner.

%sort progress {_ of ST E T} {_ of-store ST S} {_ notstuck S E} %.
%mode progress %in %in %out %.

A natural number is already a value

%term prog-int progress t-int _ (ns-isval v-int) %.

To show progress for references, we show that a new reference cell can always be created on the end of the list we use to represent the heap.

%sort lemma {_ notstuck S E} {_ notstuck S (ref E)} %.
%mode lemma %in %out %.
%term & lemma (ns-steps E) (ns-steps (s-ref E)) %.
%term &
  %pi (lemma (ns-isval V) (ns-steps (e-ref APPEND V)))
  %<- (can-append-exp EL E APPEND) %.
%worlds () (lemma _ _) %.
%total NS (lemma NS _) %.
%term prog-ref %pi (progress (t-ref T) TS NS) %<- (progress T TS NS1) %<- (lemma NS1 NS) %.

To prove progress for addition, we will need to use the fact that the subexpressions both have type int-tp—that way, once they are reduced to values, they must be numbers, not locations.

%sort lemma {_ of ST E1 int-tp} {_ notstuck S E1} {_ of ST E2 int-tp} {_ notstuck S E2} {_ notstuck S (E1 + E2)} %.
%mode lemma %in %in %in %in %out %.
%term & lemma _ (ns-steps E) _ _ (ns-steps (s1-add E)) %.
%term & lemma _ (ns-isval V) _ (ns-steps E) (ns-steps (s2-add E V)) %.
%term &
  %pi (lemma t-int (ns-isval v-int) t-int (ns-isval v-int) (ns-steps (e-add SUM)))
  %<- (can-sum N1 N2 SUM) %.
%worlds () (lemma _ _ _ _ _) %.
%total [NS1 NS2] (lemma T1 NS1 T2 NS2 NS) %.
%term prog-add
  %pi (progress (t-add T2 T1) TS NS)
  %<- (progress T1 TS NS1)
  %<- (progress T2 TS NS2)
  %<- (lemma T1 NS1 T2 NS2 NS) %.

We use both the notstuckness of the subexpressions and the ability to always project from a well-typed store (of-projection) to prove the gets case.

%sort lemma {_ of-store ST S} {_ of ST E (ref-tp T)} {_ notstuck S E} {_ notstuck S (! E)} %.
%mode lemma %in %in %in %out %.
%term & lemma _ _ (ns-steps E) (ns-steps (s-bang E)) %.
%term &
  %pi (lemma (&of-store TL VL) (t-loc PROJ-T) (ns-isval v-loc) (ns-steps (e-bang PROJ-E)))
  %<- (of-projection TL PROJ-T PROJ-E _) %.
%worlds () (lemma _ _ _ _) %.
%total NS1 (lemma ST T NS1 NS) %.
%term prog-bang %pi (progress (t-bang T) TS NS) %<- (progress T TS NS1) %<- (lemma TS T NS1 NS) %.

A location is already a value.

%term prog-loc progress (t-loc PROJ-T) TS (ns-isval v-loc) %.

We use both the notstuckness of the subexpressions and the ability to always update from a well-typed store (of-update) to prove the gets case.

%sort lemma {_ of-store ST S} {_ of ST E1 (ref-tp T)} {_ notstuck S E1} {_ notstuck S E2} {_ notstuck S (gets E1 E2)} %.
%mode lemma %in %in %in %in %out %.
%term & lemma _ _ (ns-steps E) _ (ns-steps (s1-gets E)) %.
%term & lemma _ _ (ns-isval V) (ns-steps E) (ns-steps (s2-gets E V)) %.
%term &
  %pi (lemma (&of-store TL _) (t-loc PROJ) (ns-isval v-loc) (ns-isval (%the (isval E) V)) (ns-steps (e-gets UPD V)))
  %<- (of-update TL PROJ E UPD) %.
%worlds () (lemma _ _ _ _ _) %.
%total {} (lemma _ _ _ _ _) %.
%term proj-gets
  %pi (progress (t-gets T2 T1) TS NS)
  %<- (progress T1 TS NS1)
  %<- (progress T2 TS NS2)
  %<- (lemma TS T1 NS1 NS2 NS) %.

We use a lemma about the nonstuckness of the subexpression to prove the let case.

%sort lemma {EF %pi exp %-> exp} {_ notstuck S E} {_ notstuck S (let E EF)} %.
%mode lemma %in %in %out %.
%term & lemma _ (ns-steps E) (ns-steps (s-let E)) %.
%term & lemma _ (ns-isval V) (ns-steps (e-let V)) %.
%worlds () (lemma _ _ _) %.
%total NS1 (lemma T NS1 NS) %.
%term prog-let %pi (progress (t-let _ T) TS NS) %<- (progress T TS NS1) %<- (lemma EF NS1 NS) %.
%worlds () (progress _ _ _) %.
%total T (progress T TS NS) %.

Substitution

As in the article on strengthening, progress will need to appeal to a simple substitution lemma.

%sort substitute {_ {x} %pi (var-of x Tp) %-> (of ST (EF x) T)} {_ of ST E Tp} {_ of ST (EF E) T} %.
%mode substitute %in %in %out %.
%term sub-refl substitute ([x] [v var-of x Tp] T) T* T %.
%term sub-sum
  %pi (substitute ([x] [v var-of x Tp] t-add (T2 x v) (T1 x v)) T* (t-add T2’ T1’))
  %<- (substitute ([x] [v var-of x Tp] T2 x v) T* T2’)
  %<- (substitute ([x] [v var-of x Tp] T1 x v) T* T1’) %.
%term sub-ref
  %pi (substitute ([x] [v var-of x Tp] t-ref (T x v)) T* (t-ref T’))
  %<- (substitute ([x] [v var-of x Tp] T x v) T* T’) %.
%term sub-bang
  %pi (substitute ([x] [v var-of x Tp] t-bang (T x v)) T* (t-bang T’))
  %<- (substitute ([x] [v var-of x Tp] T x v) T* T’) %.
%term sub-gets
  %pi (substitute ([x] [v var-of x Tp] t-gets (T2 x v) (T1 x v)) T* (t-gets T2' T1'))
  %<- (substitute ([x] [v var-of x Tp] T2 x v) T* T2')
  %<- (substitute ([x] [v var-of x Tp] T1 x v) T* T1') %.
%term sub-let
  %pi (substitute ([x] [v var-of x Tp] t-let (F x v) (T x v)) T* (t-let F’ T’))
  %<- (substitute ([x] [v var-of x Tp] T x v) T* T’)
  %<- ({x’} {v’ var-of x’ Tp2} substitute ([x] [v var-of x Tp] F x v x’ v’) T* (F’ x’ v’)) %.
%term sub-var substitute ([x] [v var-of x Tp] t-var v) T* T* %.
%worlds (var-tp) (substitute _ _ _) %.
%total F (substitute F T T’) %.

Weakening

In order to be able to evaluate reference cells, we need to be able to show that adding new things to the store typing will leave all current programs well-typed. The only interesting case is weak-loc.

%sort weakening {_ of ST E T} {_ subset-tp ST ST’} {_ of ST’ E T} %.
%mode weakening %in %in %out %.
%term weak-var weakening (t-var V) _ (t-var V) %.
%term weak-int weakening t-int _ t-int %.
%term weak-ref %pi (weakening (t-ref T) S (t-ref T')) %<- (weakening T S T') %.
%term weak-sum
  %pi (weakening (t-add T2 T1) S (t-add T2’ T1’))
  %<- (weakening T1 S T1’)
  %<- (weakening T2 S T2’) %.
%term weak-bang %pi (weakening (t-bang T) S (t-bang T')) %<- (weakening T S T') %.
%term weak-loc
  %pi (weakening (t-loc PROJ) S (t-loc PROJ’))
  %<- (subset-projectable PROJ S PROJ’) %.
%term weak-gets
  %pi (weakening (t-gets T2 T1) S (t-gets T2' T1'))
  %<- (weakening T2 S T2')
  %<- (weakening T1 S T1') %.
%term weak-let
  %pi (weakening (t-let F T) S (t-let F’ T’))
  %<- (weakening T S T’)
  %<- ({x} {v var-of x Tp} weakening (F x v) S (F’ x v)) %.
%worlds (var-tp) (weakening _ _ _) %.
%total T (weakening T S T’) %.

A comparable notion of weakening must be defined for lists:

%sort weakening-list {_ of-list ST EL TL} {_ subset-tp ST ST’} {_ of-list ST’ EL TL} %.
%mode weakening-list %in %in %out %.
%term weak-z weakening-list tl-z S tl-z %.
%term weak-s
  %pi (weakening-list (tl-s TL T) S (tl-s TL’ T’))
  %<- (weakening T S T’)
  %<- (weakening-list TL S TL’) %.
%worlds () (weakening-list _ _ _) %.
%total T (weakening-list T S T’) %.

Preservation

%sort preservation {_ of ST E T} {_ of-store ST S} {_ eval S E S’ E’} {_ subset-tp ST ST’} {_ of ST’ E’ T} {_ of-store ST’ S’} %.
%mode preservation %in %in %in %out %out %out %.

In the cases where evaluation is passed on to a later step, the cases are mostly a straightforward call to the induction hypothesis and the weakening lemma.

%term pres-s1-add
  %pi (preservation (t-add T2 T1) ST (s1-add E) S (t-add T2’ T1’) ST’)
  %<- (preservation T1 ST E S T1’ ST’)
  %<- (weakening T2 S T2’) %.
%term pres-s2-add
  %pi (preservation (t-add T2 T1) ST (s2-add E V) S (t-add T2’ T1’) ST’)
  %<- (preservation T2 ST E S T2’ ST’)
  %<- (weakening T1 S T1’) %.
%term pres-s-ref
  %pi (preservation (t-ref T) ST (s-ref E) S (t-ref T’) ST’)
  %<- (preservation T ST E S T’ ST’) %.
%term pres-s-bang
  %pi (preservation (t-bang T) ST (s-bang E) S (t-bang T’) ST’)
  %<- (preservation T ST E S T’ ST’) %.
%term pres-s1-gets
  %pi (preservation (t-gets T2 T1) ST (s1-gets E) S (t-gets T2' T1') ST')
  %<- (preservation T1 ST E S T1' ST')
  %<- (weakening T2 S T2') %.
%term pres-s2-gets
  %pi (preservation (t-gets T2 T1) ST (s2-gets E V) S (t-gets T2' T1') ST')
  %<- (preservation T2 ST E S T2' ST')
  %<- (weakening T1 S T1') %.
%term pres-s-let
  %pi (preservation (t-let F T) ST (s-let E) S (t-let F’ T’) ST’)
  %<- (preservation T ST E S T’ ST’)
  %<- ({x} {v} weakening (F x v) S (F’ x v)) %.

The cases where evaluation happens are more involved—for instance, the ref case relies on the very involved append-lemma from the auxillary lemmas.

%term pres-e-add
  %pi (preservation (t-add t-int t-int) ST (e-add SUM) S t-int ST)
  %<- (subset-refl _ S) %.
%term pres-e-ref
  %pi (preservation (t-ref T) (&of-store TL VL) (e-ref AE V) S (t-loc P) (&of-store TL’ VL’))
  %<- (append-lemma V T VL TL AE S VL’ TL’’ P)
  %<- (weakening-list TL’’ S TL’) %.
%term pres-e-bang
  %pi (preservation (t-bang (t-loc PROJ-T)) (&of-store TL VL) (e-bang PROJ-E) S T (&of-store TL VL))
  %<- (subset-refl _ S)
  %<- (of-projection' TL PROJ-T PROJ-E T) %.
%term pres-e-gets
  %pi (preservation (t-gets T (t-loc PROJ-T)) (&of-store TL VL) (e-gets UL V) S T (&of-store TL' VL'))
  %<- (subset-refl _ S)
  %<- (update-lemma V T VL TL PROJ-T UL VL' TL') %.
%term pres-e-let
  %pi (preservation (t-let F T’) ST (e-let V) S T ST)
  %<- (substitute F T’ T)
  %<- (subset-refl _ S) %.
%worlds () (preservation _ _ _ _ _ _) %.
%total T (preservation T ST E S T’ ST’) %.

Safety

%sort safety {_ of ST E T} {_ of-store ST S} {_ run S E S’ E’} {_ notstuck S’ E’} %.
%mode safety %in %in %in %out %.
%term safe-end %pi (safety T ST run-end NS) %<- (progress T ST NS) %.
%term safe-step
  %pi (safety T ST (run-step R E) NS)
  %<- (preservation T ST E S T’ ST’)
  %<- (safety T’ ST’ R NS) %.
%worlds () (safety _ _ _ _) %.
%total R (safety T TS R NS) %.

Example

We will define the following simple program as prog1, and use STELF’s logic programming abilities to actually run the typechecker of E T and multi-step evaluation run S E S' E'. Because gets returns the result of the assignment in the same way C does, $\texttt{}y$ should have the same value as $\texttt{}!x$ at the end of the program, namely 4.

$\begin{array}{l}\mathsf{let~}x = \mathsf{ref}(2 + 1) \mathsf{~in}\\ \mathsf{let~}y = x := !x + 1\mathsf{~in~}\\ !x + 1\end{array}$

%define prog1 let (ref (n (s (s z)) + n (s z))) ([x] let (gets x (! x + n (s z))) ([y] ! x + n (s z))) %.

We can typecheck the program (in the empty store typing nil-tp). The syntax we use for %query indicates that we only expect there to be one solution (because type checking should be syntax directed):

%query 1 _ _ of nil-tp prog1 T %.

We can then run the program to completion (starting in the empty store nil-exp). We expect the final state S to include the number 4, and we expect the program to evaluate to value V 5. The multi-step evaluation judgment run is defined to run arbitrarily until stopping, so we only want the first solution—it will be the solution resulting in running run-step as many times as possible:

%query 1 1 _ run nil-exp prog1 S V %.

References