POPL Tutorial/MinML Starter

Syntax

%sort tp %.
%name tp %.
%term num tp %.
%term arr %pi tp %-> tp %-> tp %.
%sort exp %.
%name exp %.
%term fn %pi tp %-> (%pi exp %-> exp) %-> exp %.
%term app %pi exp %-> exp %-> exp %.
%term z exp %.
%term s %pi exp %-> exp %.

Exercise: constant for ifz

%% The syntax '% .' (without the space)
%% causes Twelf to stop processing the file at this point
%% remove once you have completed the exercise

Static semantics

Exercise: typing rules for s and ifz

Dynamic semantics

value judgement

Exercise: value rules for z and s

step judgement

Exercise: step rules for s and ifz

Progress theorem

Sum type for the result

Lemmas

Exercise: lemma for s

Exercise: lemma for ifz

Main theorem

Exercise: cases for s and ifz

of : exp -> tp -> type. %name of Dof.

of/z : of z num.

of/app : of (app E1 E2) T <- of E1 (arr T’ T) <- of E2 T’.

of/fn : of (fn T1 ([x] E x)) (arr T1 T2) <- ({x:exp} of x T1 -> of (E x) T2).

%block of_block : some {T:tp} block {x:exp}{dx: of x T}. %worlds (of_block) (of _ _).

value : exp -> type. %name value Dval.

value/fn : value (fn T ([x] E x)).

step : exp -> exp -> type. %name step Dstep.

step/app/fn : 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 : step (app (fn T ([x] E x)) E2) (E E2) <- value E2.

val-or-step : exp -> type. %name val-or-step Dvos.

vos/value : val-or-step E <- value E. vos/step : val-or-step E <- step E E’.

prog/app : of E1 (arr T’ T) -> val-or-step E1 -> val-or-step E2 -> val-or-step (app E1 E2) -> type. %mode prog/app +Dof +Dvos1 +Dvos2 -Dvos.

• : prog/app _ (vos/step (Dstep1 : step E1 E1’)) _ (vos/step (step/app/fn Dstep1)).

• : prog/app _ (vos/value (Dval1 : value E1)) (vos/step (Dstep2 : step E2 E2’)) (vos/step (step/app/arg Dstep2 Dval1)).

• : prog/app (of/fn _ : of (fn T ([x] E’ x)) (arr T T’)) (vos/value (Dval1 : value (fn T ([x] E’ x)))) (vos/value (Dval2 : value E2)) (vos/step (step/app/beta Dval2)).

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

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

• : prog (of/z : of z num) (vos/value (value/z : value z)).

• : prog (of/fn _) (vos/value value/fn).

• : prog (of/app (D2 : of E2 T’) (D1 : of E1 (arr T’ T))) DvosApp <- prog D1 (Dvos1 : val-or-step E1) <- prog D2 (Dvos2 : val-or-step E2) <- prog/app D1 Dvos1 Dvos2 DvosApp.

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