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

Type safety for MinML: call-by-value, with recursive functions, in intrinsic form

Syntax / static semantics

Types:

%sort tp %.
%name tp %.
%term nat tp %.
%term arr %pi tp %-> tp %-> tp %.

Typed expressions (i.e., typing derivations):

%sort exp {_ tp} %.
%name exp %.
%prec %postfix 1 exp %.
%term z nat exp %.
%term s %pi (nat exp) %-> (nat exp) %.
%term ifz %pi (nat exp) %-> (T exp) %-> (%pi (nat exp) %-> (T exp)) %-> (T exp) %.
%term fun {T1 tp} {T2 tp} %pi (%pi (arr T1 T2 exp) %-> (T1 exp) %-> (T2 exp)) %-> (arr T1 T2 exp) %.
%term app %pi (arr T1 T2 exp) %-> (T1 exp) %-> (T2 exp) %.

Dynamic semantics / preservation

Values:

%sort value {_ T exp} %.
%name value %.
%mode value %in %.
%term value/z value z %.
%term value/s %pi (value (s E)) %<- (value E) %.
%term value/fun value (fun _ _ _) %.

Transition relation:

%sort step {_ T exp} {_ T exp} %.
%name step %.
%mode step %in %out %.
%term step/s %pi (step (s E) (s E')) %<- (step E E') %.
%term step/ifz/arg %pi (step (ifz E E1 ([x] E2 x)) (ifz E' E1 ([x] E2 x))) %<- (step E E') %.
%term step/ifz/z step (ifz z E1 ([x] E2 x)) E1 %.
%term step/ifz/s %pi (step (ifz (s E) E1 ([x] E2 x)) (E2 E)) %<- (value E) %.
%term step/app/fun %pi (step (app E1 E2) (app E1' E2)) %<- (step E1 E1') %.
%term step/app/arg %pi (step (app E1 E2) (app E1 E2')) %<- (value E1) %<- (step E2 E2') %.
%term step/app/beta-v
  %pi (step (app (fun T1 T2 ([f] [x] E f x)) E2) (E (fun T1 T2 ([f] [x] E f x)) E2))
  %<- (value E2) %.

Progress

The sum type we return:

%sort val-or-step {_ T exp} %.
%name val-or-step %.
%term vos/val %pi (val-or-step E) %<- (value E) %.
%term vos/step %pi (val-or-step E) %<- (step E _) %.

Factoring lemmas

%sort prog/s {_ val-or-step E} {_ val-or-step (s E)} %.
%mode prog/s %in %out %.
%term _ prog/s (vos/step Dstep) (vos/step (step/s Dstep)) %.
%term _ prog/s (vos/val Dval) (vos/val (value/s Dval)) %.
%worlds () (prog/s _ _) %.
%total {} (prog/s _ _) %.
%sort prog/ifz {_ val-or-step (%the (nat exp) E)} {E1} {E2} {_ step (ifz E E1 ([x] E2 x)) E'} %.
%mode prog/ifz %in %in %in %out %.
%term _ prog/ifz (vos/step Dstep) _ _ (step/ifz/arg Dstep) %.
%term _ prog/ifz (vos/val value/z) _ _ step/ifz/z %.
%term _ prog/ifz (vos/val (value/s Dval)) _ _ (step/ifz/s Dval) %.
%worlds () (prog/ifz _ _ _ _) %.
%total {} (prog/ifz _ _ _ _) %.
%sort prog/app {_ val-or-step (%the (arr T2 T exp) E1)} {_ val-or-step (%the (T2 exp) E2)} {_ step (app E1 E2) E'} %.
%mode prog/app %in %in %out %.
%term _ prog/app (vos/step Dstep1) _ (step/app/fun Dstep1) %.
%term _ prog/app (vos/val Dval1) (vos/step Dstep2) (step/app/arg Dstep2 Dval1) %.
%term _ prog/app (vos/val Dval1) (vos/val Dval2) (step/app/beta-v Dval2) %.
%worlds () (prog/app _ _ _) %.
%total {} (prog/app _ _ _) %.

Main theorem

%sort prog {E T exp} {_ val-or-step E} %.
%name prog %.
%mode prog %in %out %.
%term _ prog z (vos/val value/z) %.
%term _ %pi (prog (s E) Dvos') %<- (prog E Dvos) %<- (prog/s Dvos Dvos') %.
%term _
  %pi (prog (ifz E E1 ([x] E2 x)) (vos/step Dstep))
  %<- (prog E Dvos)
  %<- (prog/ifz Dvos _ _ Dstep) %.
%term _ prog (fun _ _ _) (vos/val value/fun) %.
%term _
  %pi (prog (app E1 E2) (vos/step Dstep))
  %<- (prog E1 Dvos1)
  %<- (prog E2 Dvos2)
  %<- (prog/app Dvos1 Dvos2 Dstep) %.
%worlds () (prog _ _) %.
%total Dof (prog Dof _) %.

And thus we have proved type safety for MinML!