POPL Tutorial/MinML Starter

This is Literate Twelf Code: here Status: %% OK %% Output: here.

Syntax

tp : type.				%name tp T.
num : tp.
arr : tp -> tp -> tp.

exp : type.				%name exp E.
fn : tp -> (exp -> exp) -> exp.
app : exp -> exp -> exp.
z : exp.
s : 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

}%

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).

%{

Exercise: typing rules for s and ifz

}%

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

%{

Dynamic semantics

value judgement

}%

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

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

Exercise: value rules for z and s

}%

%{

step judgement

}%

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.

%{

Exercise: step rules for s and ifz

}%

%{

Progress theorem

Sum type for the result

}%

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

%{

Lemmas

}%

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 _ _ _ _).

%{

Exercise: lemma for s

}%

%{

Exercise: lemma for ifz

}%

%{

Main theorem

}%

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.

%{

Exercise: cases for s and ifz

}%

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