Summer school 2008:Type safety for polymorphic MinML (intrinsic encoding)

This is Literate Twelf Code: here Status: %% OK %% Output: here.

MinML: call-by-value, with recursive functions, using an intrinsic encoding

Types

tp : type.				%name tp T.
nat : tp.
arr : tp -> tp -> tp.
all : (tp -> tp) -> tp.

Syntax / static semantics

exp : tp -> type.			%name exp E.

z : exp nat.
s : exp nat -> exp nat.
ifz : exp nat -> exp T -> (exp nat -> exp T) -> exp T.
fun : {T1} {T2} (exp (arr T1 T2) -> exp T1 -> exp T2) -> exp (arr T1 T2).
app : exp (arr T2 T) -> exp T2 -> exp T.
tfun : ({a : tp} exp (T a)) -> exp (all [a] T a).
tapp : exp (all [a] T a) -> {T2 : tp} exp (T T2).

Dynamic Semantics / Preservation

value : exp T -> type.			%name value Dval.
%mode value +E.

value/z : value z.
value/s : value (s E) <- value E.
value/fun : value (fun _ _ _).
value/tfun : value (tfun _).

step : exp T -> exp T -> type.		%name step Dstep.
%mode step +E1 -E2.

step/s
   : step (s E) (s E') <- step E E'.
step/ifz/arg
   : step (ifz E E1 ([x] E2 x)) (ifz E' E1 ([x] E2 x))
      <- step E E'.
step/ifz/z
   : step (ifz z E1 ([x] E2 x)) E1.
step/ifz/s
   : step (ifz (s E) E1 ([x] E2 x)) (E2 E)
      <- value E.
step/app/fun
   : step (app E1 E2) (app E1' E2)
      <- step E1 E1'.
step/app/arg
   : step (app E1 E2) (app E1 E2')
      <- value E1 <- step E2 E2'.
step/app/beta-v
   : step
      (app (fun T1 T2 ([f] [x] E f x)) E2)
      (E (fun T1 T2 ([f] [x] E f x)) E2)
      <- value E2.
step/tapp/tfun
   : step (tapp E T) (tapp E' T)
      <- step E E'.
step/tapp/beta
   : step (tapp (tfun ([a] E a)) T) (E T).

Progress

val-or-step : exp T -> type.		%name val-or-step Dvos.
vos/val : val-or-step E <- value E.
vos/step : val-or-step E <- step E _.

Factoring lemmas

These are necessary for case-analyzing the results of recursive calls.

prog/s
   : val-or-step E -> val-or-step (s E) -> type.
%mode prog/s +Dvos1 -Dvos2.

- : prog/s
     (vos/step Dstep)
     (vos/step (step/s Dstep)).

- : prog/s
     (vos/val Dval)
     (vos/val (value/s Dval)).

%worlds () (prog/s _ _).
%total {} (prog/s _ _).

prog/ifz : val-or-step (E : exp nat)
	    -> {E1} {E2}
	       step (ifz E E1 ([x] E2 x)) E'
	    -> type.
%mode prog/ifz +E +E1 +E2 -Dstep.

- : prog/ifz (vos/step Dstep) _ _ (step/ifz/arg Dstep).

- : prog/ifz (vos/val value/z) _ _ step/ifz/z.

- : prog/ifz (vos/val (value/s Dval)) _ _ (step/ifz/s Dval).

%worlds () (prog/ifz _ _ _ _).
%total {} (prog/ifz _ _ _ _).

prog/app : val-or-step (E1 : exp (arr T2 T))
	    -> val-or-step E2
	    -> step (app E1 E2) E'
	    -> type.
%mode prog/app +Dvos1 +Dvos2 -Dstep.

- : prog/app
     (vos/step Dstep1)
     _
     (step/app/fun Dstep1).

- : prog/app
     (vos/val Dval1)
     (vos/step Dstep2)
     (step/app/arg Dstep2 Dval1).

- : prog/app
     (vos/val Dval1)
     (vos/val Dval2)
     (step/app/beta-v Dval2).

%worlds () (prog/app _ _ _).
%total {} (prog/app _ _ _).

prog/tapp : val-or-step (E : exp (all [a] T a))
	    -> {T'} 
	       {E'}  %% otherwise, the type of E' can't mention T'
	       step (tapp E T') E'   
	    -> type.
%mode prog/tapp +E +T' -E' -Dstep.

- : prog/tapp
     (vos/step Dstep1)
     _ _
     (step/tapp/tfun Dstep1).

- : prog/tapp
     (vos/val Dval)
     _ _
     step/tapp/beta.

%worlds () (prog/tapp _ _ _ _).
%total {} (prog/tapp _ _ _ _).

Main theorem

prog : {E : exp T} val-or-step E -> type. 
%mode prog +Dof -Dvos.

- : prog z (vos/val value/z).

- : prog (s E') Dvos'
     <- prog E' Dvos
     <- prog/s Dvos Dvos'.

- : prog (ifz E E0 ([x] E1 x)) (vos/step Dstep)
     <- prog E Dvos
     <- prog/ifz Dvos _ _ Dstep.

- : prog (fun _ _ _) (vos/val value/fun).

- : prog (app E1 E2) (vos/step Dstep)
     <- prog E1 Dvos1
     <- prog E2 Dvos2
     <- prog/app Dvos1 Dvos2 Dstep.

- : prog (tfun _) (vos/val value/tfun).

- : prog (tapp E T) (vos/step Dstep)
     <- prog E Dvos
     <- prog/tapp Dvos _ _ Dstep.

%worlds () (prog _ _).
%total Dof (prog Dof _).

And thus we have proved type safety for MinML with polymorphism!