POPL Tutorial/MinML Preservation Theorem: Solution

From The Twelf Project

This is the solution to this exercise.

Type safety for MinML

Preservation

pres : step E E' -> of E T -> of E' T -> type. %name pres Dpres.
%mode pres +Dstep +Dof -Dof.

- : pres
     (step/s Dstep)
     (of/s Dof)
     (of/s Dof')
     <- pres Dstep Dof Dof'.

- : 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'.

- : pres
     step/ifz/z
     (of/ifz _ Dof1 _)
     Dof1.

- : pres
     (step/ifz/s (_ : value E))
     (of/ifz ([x] [dx] Dof2 x dx) _ (of/s Dof))
     (Dof2 E Dof).

- : pres
     (step/app/fn Dstep1)
     (of/app Dof2 Dof1)
     (of/app Dof2 Dof1')
     <- pres Dstep1 Dof1 Dof1'.

- : pres
     (step/app/arg Dstep2 _)
     (of/app Dof2 Dof1)
     (of/app Dof2' Dof1)
     <- pres Dstep2 Dof2 Dof2'.

- : pres
     (step/app/beta _)
     (of/app
	Dof2
	(of/fn [x] [dx] (Dof1 x dx)))
     (Dof1 _ Dof2).

%worlds () (pres Dstep Dof Dof').
%total Dstep (pres Dstep _ _).