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

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

Syntax

Types:

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

Raw expressions, which admit ill-typed terms

%sort exp %.
%name exp %.
%term z exp %.
%term s %pi exp %-> exp %.
%term ifz %pi exp %-> exp %-> (%pi exp %-> exp) %-> exp %.
%term fun %pi tp %-> tp %-> (%pi exp %-> exp %-> exp) %-> exp %.
%term app %pi exp %-> exp %-> exp %.

Static semantics

A judgement picking out the well-typed terms:

%sort of {_ exp} {_ tp} %.
%name of %.
%mode of %in %out %.
%term of/z of z nat %.
%term of/s %pi (of (s E) nat) %<- (of E nat) %.
%term of/ifz
  %pi (of (ifz E E1 ([x] E2 x)) T)
  %<- (of E nat)
  %<- (of E1 T)
  %<- ({x exp} %pi (of x nat) %-> (of (E2 x) T)) %.
%term of/fun
  %pi (of (fun T1 T2 ([f] [x] E f x)) (arr T1 T2))
  %<- ({f exp} %pi (of f (arr T1 T2)) %-> ({x exp} %pi (of x T1) %-> (of (E f x) T2))) %.
%term of/app %pi (of (app E1 E2) T) %<- (of E1 (arr T2 T)) %<- (of E2 T2) %.

Dynamic semantics

%sort value {_ 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 _ _ _) %.
%sort step {_ exp} {_ 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) %.

Preservation

With this encoding, we have to prove preservation explicitly, as the type of step doesn’t guarantee it.

%sort pres {_ step E E'} {_ of E T} {_ of E' T} %.
%name pres %.
%mode pres %in %in %out %.
%term _ %pi (pres (step/s Dstep) (of/s Dof) (of/s Dof')) %<- (pres Dstep Dof Dof') %.
%term _
  %pi (pres (step/ifz/arg Dstep) (of/ifz ([x] [dx] Dof2 x dx) Dof1 Dof) (of/ifz ([x] [dx] Dof2 x dx) Dof1 Dof'))
  %<- (pres Dstep Dof Dof') %.
%term _ pres step/ifz/z (of/ifz _ Dof1 _) Dof1 %.
%term _ pres (step/ifz/s (%the (value E) _)) (of/ifz ([x] [dx] Dof2 x dx) _ (of/s Dof)) (Dof2 E Dof) %.
%term _
  %pi (pres (step/app/fun Dstep1) (of/app Dof2 Dof1) (of/app Dof2 Dof1'))
  %<- (pres Dstep1 Dof1 Dof1') %.
%term _
  %pi (pres (step/app/arg Dstep2 _) (of/app Dof2 Dof1) (of/app Dof2' Dof1))
  %<- (pres Dstep2 Dof2 Dof2') %.
%term _ pres (step/app/beta-v _) (of/app Dof2 (of/fun ([f] [df] [x] [dx] Dof1 f df x dx))) (Dof1 _ (of/fun ([f] [df] [x] [dx] Dof1 f df x dx)) _ Dof2) %.
%worlds () (pres Dstep Dof Dof') %.
%total Dstep (pres Dstep _ _) %.

Progress

%sort val-or-step {_ 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 {_ of E nat} {_ val-or-step E} {E1} {E2} {_ step (ifz E E1 ([x] E2 x)) E'} %.
%mode prog/ifz %in %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 {_ of E1 (arr T2 T)} {_ val-or-step E1} {_ val-or-step E2} {_ step (app E1 E2) E'} %.
%mode prog/app %in %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 {_ of E T} {_ val-or-step E} %.
%name prog %.
%mode prog %in %out %.
%term _ prog of/z (vos/val value/z) %.
%term _ %pi (prog (of/s Dof) Dvos') %<- (prog Dof Dvos) %<- (prog/s Dvos Dvos') %.
%term _
  %pi (prog (of/ifz ([x] [dx] Dof2 x dx) Dof1 Dof) (vos/step Dstep))
  %<- (prog Dof Dvos)
  %<- (prog/ifz Dof Dvos _ _ Dstep) %.
%term _ prog (of/fun _) (vos/val value/fun) %.
%term _
  %pi (prog (of/app Dof2 Dof1) (vos/step Dstep))
  %<- (prog Dof1 Dvos1)
  %<- (prog Dof2 Dvos2)
  %<- (prog/app Dof1 Dvos1 Dvos2 Dstep) %.
%worlds () (prog _ _) %.
%total Dof (prog Dof _) %.

And thus we have proved type safety for minml!

Examples

%inline plus (exp) fun nat (arr nat nat) ([plus] [x] ifz x (fun nat nat ([_] [y] y)) ([predx] fun nat nat ([_] [y] s (app (app plus predx) y)))) %.
%solve D : of plus T %.
%inline mult (exp) fun nat (arr nat nat) ([mult] [x] fun nat nat ([_] [y] ifz y z ([predy] app (app plus x) (app (app mult x) predy)))) %.
%solve Dmult : of mult T %.
%inline fact (exp) fun nat nat ([fact] [x] ifz x (s z) ([predx] app (app mult x) (app fact predx))) %.
%solve Dfact : of fact T %.
%sort stepv {_ exp} {_ exp} %.
%term stepv/v %pi (stepv E E) %<- (value E) %.
%term stepv/s %pi (stepv E E'') %<- (step E E') %<- (stepv E' E'') %.
%solve D : stepv (app (app plus (s (s z))) (s (s z))) E %.
%solve D : stepv (app (app mult (s (s (s z)))) (s (s z))) E %.
%solve D : stepv (app fact (s (s (s z)))) E %.