miniml.elf

% Core Mini-ML

% --- syntax

exp : type.
z : exp.
s : exp -> exp.
case : exp -> exp -> (exp -> exp) -> exp.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.
fix : (exp -> exp) -> exp.

% --- operational semantics

eval : exp -> exp -> type.
ev_z : eval z z.
ev_s : eval (s E) (s V)
       <- eval E V.

ev_case_z : eval (case E E1 ([x] E2 x)) V
	     <- eval E z
	     <- eval E1 V.
ev_case_s : eval (case E E1 E2) V
	     <- eval E (s V')
	     <- eval (E2 V') V.

ev_lam : eval (lam [x]E x) (lam [x]E x).

ev_app : eval (app E1 E2) V
	  <- eval E1 (lam E1')
	  <- eval E2 V'
	  <- eval (E1' V') V.

ev_fix : eval (fix [x]E x) V
          <- eval (E (fix [x] E x)) V.

%query 1 * D : eval (app (lam [x] s x) z) V.

% --- notion of value

value : exp -> type.

val_z : value z.

val_s : value (s V)
	 <- value V.

val_lam : value (lam [x] E x).

% --- type system

tp : type.

nat : tp.

arrow : tp -> tp -> tp.

of : exp -> tp -> type.

of_z : of z nat.

of_s : of (s E) nat
	<- of E nat.

of_case : of (case E E1 [x]E2 x) T
             <-	of E nat
             <- of E1 T
             <- ({x:exp} of x nat -> of (E2 x) T).

of_lam : of (lam [x] E x) (arrow T T')
	  <- {x:exp} of x T -> of (E x) T'.

of_app : of (app E1 E2) T'
	  <- of E1 (arrow T T')
	  <- of E2 T.

of_fix : of (fix [x] E x) T
	  <- {x:exp} of x T -> of (E x) T.

myexp : exp = lam[x] case x (s z) [y] z.

%query 1 5 D : of myexp T.