Mutable state

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.

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,[1] 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.[2] 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.)

nat : type.
z : nat. 
s : nat -> nat. 

sum : nat -> nat -> nat -> type. 
%mode sum +A +B -C. 
sum-z : sum z N N. 
sum-s : 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 , where is a natural number 0, 1, 2...
  • E1 + E2 - addition,
  • ref E - creating a reference cell,
  • ! E - dereferencing a reference cell,
  • gets E1 E2 - updating a reference cell,
  • loc L - locations (not available to the programmer), , where is an abstract location.
  • let E1 ([x] E2 x) - let statements
%abbrev location = nat. 
exp : type. 
n : nat -> exp. 
+ : exp -> exp -> exp. %infix left 10 +. 
ref : exp -> exp. 
! : exp -> exp. 
gets : exp -> exp -> exp. 
loc : location -> exp. 
let : exp -> (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.

tp : type. 
int-tp : tp. 
ref-tp : tp -> tp.

Lists

We will represent the store as a list of expressions, and define several operations on lists—projecting the nth element from a list, appending a new element to the end of a list, updating the nth 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.

explist : type. 

$exp : exp -> explist -> explist.  %infix right 5 $exp. 
nil-exp : explist. 


proj-exp : explist -> nat -> exp -> type. 
%mode proj-exp +EL +N -E. 
proj-exp-z : proj-exp (E $exp EL) z E. 
proj-exp-s : proj-exp (E $exp EL) (s N) E’ 
	     <- proj-exp EL N E’. 


append-exp : explist -> exp -> explist -> nat -> type. 
%mode append-exp +EL +E -EL’ -N. 
append-exp-z : append-exp nil-exp E (E $exp nil-exp) z. 
append-exp-s : append-exp (E’ $exp EL) E (E’ $exp EL’) (s N) 
		<- append-exp EL E EL’ N. 


subset-exp : explist -> explist -> type. 
%mode subset-exp +EL +EL'.
subset-exp-z : subset-exp nil-exp E. 
subset-exp-s : subset-exp (E $exp EL) (E $exp EL’) 
		<- subset-exp EL EL’. 


update-exp : explist -> nat -> exp -> explist -> type.
%mode update-exp +EL +N +E -EL'.
update-exp-z : update-exp (E $exp EL) z E' (E' $exp EL).
update-exp-s : update-exp (E $exp EL) (s N) E' (E $exp EL')
	       <- update-exp EL N E' EL'.


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

%abbrev store = explist. 
%abbrev storetp = tplist.

Values and evaluation

The predicate isval

isval : exp -> type. 
%mode isval +E. 
v-int : isval (n N). 
v-loc : isval (loc L). 

isval-list : explist -> type. 
%mode isval-list +E. 
vl-z : isval-list nil-exp. 
vl-s : isval-list (E $exp EL) 
	<- isval E 
	<- isval-list EL. 

eval : store -> exp -> store -> exp -> type. 
%mode eval +S +E -S’ -E’. 

s1-add : eval S (E1 + E2) S’ (E1’ + E2) 
	  <- eval S E1 S’ E1’. 
s2-add : eval S (E1 + E2) S’ (E1 + E2’) 
	  <- isval E1 
	  <- eval S E2 S’ E2’. 
e-add : eval S (n N1 + n N2) S (n N3) 
	 <- sum N1 N2 N3. 
s-ref : eval S (ref E) S’ (ref E’) 
	 <- eval S E S’ E’. 
e-ref : eval S (ref E) S’ (loc L) 
	 <- isval E 
	 <- append-exp S E S’ L. 
s-bang : eval S (! E) S’ (! E’) 
	  <- eval S E S’ E’. 
e-bang : eval S (! (loc L)) S E 
	  <- proj-exp S L E. 
s1-gets : eval S (gets E1 E2) S' (gets E1' E2)
	   <- eval S E1 S' E1'.
s2-gets : eval S (gets E1 E2) S' (gets E1 E2')
	   <- isval E1
	   <- eval S E2 S' E2'.
e-gets : eval S (gets (loc L1) E) S' E
	  <- isval E
	  <- update-exp S L1 E S'.
s-let : eval S (let E EF) S’ (let E’ EF) 
	 <- eval S E S’ E’. 
e-let : 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.

var-of : exp -> tp -> type. 
%mode var-of +E -T. 
of : storetp -> exp -> tp -> type. 
%mode of +ST +E -T. 
of-list : storetp -> explist -> tplist -> type. 
%mode of-list +ST +E -T. 


tl-z : of-list ST nil-exp nil-tp. 
tl-s : of-list ST (E $exp EL) (T $tp TL) 
	<- of ST E T 
	<- of-list ST EL TL. 


t-int : of ST (n N) int-tp. 
t-add : of ST (E1 + E2) int-tp 
	 <- of ST E1 int-tp 
	 <- of ST E2 int-tp. 
t-ref : of ST (ref E) (ref-tp T) 
	 <- of ST E T. 
t-bang : of ST (! E) T 
	  <- of ST E (ref-tp T). 
t-gets : of ST (gets E1 E2) T
	  <- of ST E1 (ref-tp T)
	  <- of ST E2 T.
t-loc : of ST (loc L) (ref-tp T) 
	 <- proj-tp ST L T. 
t-let : of ST (let E EF) T 
	 <- of ST E T’ 
	 <- ({x} var-of x T’ -> of ST (EF x) T). 
t-var : 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 : some {T:tp} block {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.

of-store : storetp -> store -> type. 
&of-store : of-store TL EL 
	     <- isval-list EL 
	     <- of-list TL EL TL.

Multi-step evaluation

run : store -> exp 
	    -> store -> exp -> type. 
%mode run +S +E -S’ -E’. 
run-step : run S E S’’ E’’ 
	    <- eval S E S’ E’ 
	    <- run S’ E’ S’’ E’’. 
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.

can-sum : {A: nat}{B: nat} sum A B C -> type. 
%mode can-sum +A +B -SUM. 
& : can-sum z N sum-z. 
& : can-sum (s N1) N2 (sum-s SUM) 
<- can-sum N1 N2 SUM. 
%worlds () (can-sum _ _ _). 
%total T (can-sum T _ _). 


can-append-exp : {EL:explist}{E:exp} append-exp EL E EL' N -> type.
%mode can-append-exp +EL +E -APPEND.
& : can-append-exp nil-exp E append-exp-z.
& : 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

of-projection : of-list ST EL TL 
		 -> proj-tp TL N T 
		 %% implies
		 -> proj-exp EL N E 
		 -> of ST E T -> type. 
%mode of-projection +TL +PT -PE -T. 
& : of-projection (tl-s TL T) proj-tp-z proj-exp-z T. 
& : 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 _ _). 

of-projection' : of-list ST EL TL 
		 -> proj-tp TL N T 
		 %% implies
		 -> proj-exp EL N E 
		 -> of ST E T -> type. 
%mode of-projection' +TL +PT +PE -T. 
& : of-projection' (tl-s TL T) proj-tp-z proj-exp-z T. 
& : 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 _ _). 

subset-projectable : proj-tp ST N T 
		      -> subset-tp ST ST’ 
		      -> proj-tp ST’ N T -> type. 
%mode subset-projectable +P +S -P’. 
& : subset-projectable proj-tp-z (subset-tp-s SUB) proj-tp-z. 
& : 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’). 


subset-refl : {ST} subset-tp ST ST -> type. 
%mode subset-refl +ST -S. 
& : subset-refl nil-tp subset-tp-z.
& : subset-refl (T $tp ST) (subset-tp-s SUB)
     <- subset-refl ST SUB.
%worlds () (subset-refl _ _).
%total T (subset-refl T _).

of-update : of-list ST EL TL 
	     -> proj-tp TL L T
	     %% implies
	     -> {E} update-exp EL L E EL' 
	     -> type.
%mode of-update +T +PT +E -PE.
& : of-update (tl-s _ _) proj-tp-z _ update-exp-z.
& : 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 _ _ _).



append-lemma : isval E 
		-> of ST E T 
		-> isval-list EL 
		-> of-list ST EL TL 
		-> append-exp EL E EL’ N 
		%% implies
		-> subset-tp TL TL’ 
		-> isval-list EL’ 
		-> of-list ST EL’ TL’ 
		-> proj-tp TL’ N T -> type. 
%mode append-lemma +V +T +VL +TL +AE -S -VL’ -TL’ -P. 
& : 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. 
& : 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). 



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'
		%% implies
		-> isval-list EL'
		-> of-list ST EL' TL -> type.
%mode update-lemma +V +T +VL +TL +P +UE -TL' -VL'.
& : 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).
& : 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.

notstuck : store -> exp -> type. 
ns-steps : notstuck S E 
	    <- eval S E S’ E’. 
ns-isval : notstuck S E 
	    <- isval E.

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

progress : of ST E T 
	    -> of-store ST S 
	    %% implies
	    -> notstuck S E -> type. 
%mode progress +T +TS -NS.

A natural number is already a value

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.

lemma : notstuck S E -> notstuck S (ref E) -> type. 
%mode lemma +NS1 -NS. 
& : lemma (ns-steps E) (ns-steps (s-ref E)). 
& : lemma (ns-isval V) (ns-steps (e-ref APPEND V)) 
     <- can-append-exp EL E APPEND. 
%worlds () (lemma _ _). %total NS (lemma NS _). 
prog-ref : 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.

lemma : of ST E1 int-tp
	 -> notstuck S E1 
	 -> of ST E2 int-tp
	 -> notstuck S E2 
	 %% implies
	 -> notstuck S (E1 + E2) -> type. 
%mode lemma +T1 +NS1 +T2 +NS2 -NS. 
& : lemma _ (ns-steps E) _ _ (ns-steps (s1-add E)). 
& : lemma _ (ns-isval V) _ (ns-steps E) (ns-steps (s2-add E V)). 
& : 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). 
prog-add : 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.

lemma : of-store ST S 
	 -> of ST E (ref-tp T) 
	 -> notstuck S E 
	 %% implies
	 -> notstuck S (! E) -> type. 
%mode lemma +ST +T +NS1 -NS. 
& : lemma _ _ (ns-steps E) (ns-steps (s-bang E)). 
& : 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). 
prog-bang : progress (t-bang T) TS NS 
	     <- progress T TS NS1 
	     <- lemma TS T NS1 NS.

A location is already a value.

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.

lemma : of-store ST S 
	 -> of ST E1 (ref-tp T) 
	 -> notstuck S E1
	 -> notstuck S E2
	 %% implies
	 -> notstuck S (gets E1 E2) -> type.
%mode lemma +TL +T +NS1 +NS2 -NS.
& : lemma _ _ (ns-steps E) _ (ns-steps (s1-gets E)).
& : lemma _ _ (ns-isval V) (ns-steps E) (ns-steps (s2-gets E V)).
& : lemma (&of-store TL _) (t-loc PROJ) (ns-isval v-loc) 
     (ns-isval (V:isval E)) (ns-steps (e-gets UPD V))
     <- of-update TL PROJ E UPD.
%worlds () (lemma _ _ _ _ _).
%total {} (lemma _ _ _ _ _).
proj-gets : 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.

lemma : {EF: exp -> exp} notstuck S E -> notstuck S (let E EF) -> type. 
%mode lemma +EF +NS1 -NS. 
& : lemma _ (ns-steps E) (ns-steps (s-let E)). 
& : lemma _ (ns-isval V) (ns-steps (e-let V)). 
%worlds () (lemma _ _ _). %total NS1 (lemma T NS1 NS). 
prog-let : 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.

substitute : ({x} var-of x Tp -> of ST (EF x) T) 
	      -> of ST E Tp 
	      %% implies
	      -> of ST (EF E) T -> type. 
%mode substitute +F +T -T’. 

sub-refl : substitute ([x][v: var-of x Tp] T) T* T. 
sub-sum : 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’. 
sub-ref : 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’. 
sub-bang : 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’. 
sub-gets : 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'. 
sub-let : 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’). 
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.

weakening : of ST E T -> subset-tp ST ST’ -> of ST’ E T -> type. 
%mode weakening +T +SUB -T’. 

weak-var : weakening (t-var V) _ (t-var V).
weak-int : weakening (t-int) _ (t-int).
weak-ref : weakening (t-ref T) S (t-ref T')
	    <- weakening T S T'.
weak-sum : weakening (t-add T2 T1) S (t-add T2’ T1’) 
	    <- weakening T1 S T1’ 
	    <- weakening T2 S T2’. 
weak-bang : weakening (t-bang T) S (t-bang T')
	     <- weakening T S T'.
weak-loc : weakening (t-loc PROJ) S (t-loc PROJ’) 
	    <- subset-projectable PROJ S PROJ’. 
weak-gets : weakening (t-gets T2 T1) S (t-gets T2' T1')
	     <- weakening T2 S T2'
	     <- weakening T1 S T1'.
weak-let : 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:

weakening-list : of-list ST EL TL 
		  -> subset-tp ST ST’ 
		  -> of-list ST’ EL TL -> type. 
%mode weakening-list +T +SUB -T’. 
weak-z : weakening-list tl-z S tl-z. 
weak-s : 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

preservation : of ST E T 
		-> of-store ST S 
		-> eval S E S’ E’ 
		%% implies
		-> subset-tp ST ST’ 
		-> of ST’ E’ T 
		-> of-store ST’ S’ -> type. 
%mode preservation +T +TS +E -S -T’ -TS’.

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.

pres-s1-add : 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’. 
pres-s2-add : 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’. 
pres-s-ref : preservation (t-ref T) ST (s-ref E) S (t-ref T’) ST’ 
	      <- preservation T ST E S T’ ST’. 
pres-s-bang : preservation (t-bang T) ST (s-bang E) S (t-bang T’) ST’ 
	       <- preservation T ST E S T’ ST’. 
pres-s1-gets : 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'.
pres-s2-gets : 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'.
pres-s-let : 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.

pres-e-add : preservation (t-add t-int t-int) ST (e-add SUM) S t-int ST 
	      <- subset-refl _ S. 
pres-e-ref : 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’. 
pres-e-bang : 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.
pres-e-gets : 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'.
pres-e-let : 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

safety : of ST E T 
	  -> of-store ST S 
	  -> run S E S’ E’ 
	  -> notstuck S’ E’ -> type. 
%mode safety +T +TS +R -NS. 
safe-end : safety T ST run-end NS 
	    <- progress T ST NS. 
safe-step : 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 Twelf'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, should have the same value as at the end of the program, namely 4.

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).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%query 1 * of nil-tp prog1 T. ---------- Solution 1 ---------- T = int-tp. ____________________________________________

%% OK %%

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).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%query 1 1 run nil-exp prog1 S V. ---------- Solution 1 ---------- V = n (s (s (s (s (s z))))); S = n (s (s (s (s z)))) $exp nil-exp. ____________________________________________

%% OK %%

References

  1. Robert J. Simmons - Twelf as a Unified Framework for Language Formalization and Implementation
    Technical Report, Princeton University ,2005
    Bibtex
    Author : Robert J. Simmons
    Title : Twelf as a Unified Framework for Language Formalization and Implementation
    In : Technical Report, Princeton University -
    Address :
    Date : 2005
  2. Benjamin C. Pierce - Types and Programming Languages
    MIT Press, February 2002
    Bibtex
    Author : Benjamin C. Pierce
    Title : Types and Programming Languages
    In : -
    Address :
    Date : February 2002

Read more Twelf case studies and other Twelf documentation.