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

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

Types

%sort tp %.
%name tp %.
%term nat tp %.
%term arr %pi tp %-> tp %-> tp %.
%term all %pi (%pi tp %-> tp) %-> tp %.

Syntax / static semantics

%sort exp {_ tp} %.
%name exp %.
%term z exp nat %.
%term s %pi (exp nat) %-> (exp nat) %.
%term ifz %pi (exp nat) %-> (exp T) %-> (%pi (exp nat) %-> (exp T)) %-> (exp T) %.
%term fun {T1} {T2} %pi (%pi (exp (arr T1 T2)) %-> (exp T1) %-> (exp T2)) %-> (exp (arr T1 T2)) %.
%term app %pi (exp (arr T2 T)) %-> (exp T2) %-> (exp T) %.
%term tfun %pi ({a tp} exp (T a)) %-> (exp (all ([a] T a))) %.
%term tapp %pi (exp (all ([a] T a))) %-> ({T2 tp} exp (T T2)) %.

Dynamic Semantics / Preservation

%sort value {_ exp T} %.
%name value %.
%mode value %in %.
%term value/z value z %.
%term value/s %pi (value (s E)) %<- (value E) %.
%term value/fun value (fun _ _ _) %.
%term value/tfun value (tfun _) %.
%sort step {_ exp T} {_ exp T} %.
%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) %.
%term step/tapp/tfun %pi (step (tapp E T) (tapp E' T)) %<- (step E E') %.
%term step/tapp/beta step (tapp (tfun ([a] E a)) T) (E T) %.

Progress

%sort val-or-step {_ exp T} %.
%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

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

%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 (exp nat) 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 (exp (arr T2 T)) E1)} {_ val-or-step 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 _ _ _) %.
%sort prog/tapp {_ val-or-step (%the (exp (all ([a] T a))) E)} {T'} {E'} {_ step (tapp E T') E'} %.
%mode prog/tapp %in %in %out %out %.
%term _ prog/tapp (vos/step Dstep1) _ _ (step/tapp/tfun Dstep1) %.
%term _ prog/tapp (vos/val Dval) _ _ step/tapp/beta %.
%worlds () (prog/tapp _ _ _ _) %.
%total {} (prog/tapp _ _ _ _) %.

Main theorem

%sort prog {E exp T} {_ val-or-step E} %.
%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 E0 ([x] E1 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) %.
%term _ prog (tfun _) (vos/val value/tfun) %.
%term _
  %pi (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!