A summary of the first two weeks of CMU's 15-312

pl.elf

nat : type.
s   : nat -> nat.
z   : nat.

bool  : type.
true  : bool.
false : bool.

plus : nat -> nat -> nat -> type.
%mode plus +N +M -R.

plus/z : plus z N N.
plus/s : plus (s N) M (s E)
          <- plus N M E.

%worlds () (plus _ _ _).
%total N (plus N _ _).

ty      : type.
ty/bool : ty.
ty/nat  : ty.

exp   : type.
exp/n : nat -> exp.
exp/b : bool -> exp.
exp/+ : exp -> exp -> exp.
exp/l : exp -> (exp -> exp) -> exp.
exp/i : exp -> exp -> exp -> exp.

of    : exp -> ty -> type.
of/n  : {n} of (exp/n n) ty/nat.
of/b  : {B} of (exp/b B) ty/bool.
of/+  : of L ty/nat -> of R ty/nat -> of (exp/+ L R) ty/nat.
of/l : of (exp/l B F) T
         <- ({e : exp} of e T' -> of (F e) T)
         <- of B T'.
of/i : of If ty/bool -> of Th T -> of El T -> of (exp/i If Th El) T.

value : exp -> type.
value/n : {N} value (exp/n N).
value/b : {B} value (exp/b B).

step : exp -> exp -> type.
step/+1  : step (exp/+ L R) (exp/+ L' R)
            <- step L L'.
step/+2  : step (exp/+ L R) (exp/+ L R')
            <- value L
            <- step R R'.
step/+3  : step (exp/+ (exp/n L) (exp/n R)) (exp/n E)
            <- plus L R E.
step/l1 : step (exp/l E F) (exp/l E' F)
           <- step E E'.
step/l2 : step (exp/l V F) (F V)
           <- value V.
step/i1 : step (exp/i If Th El) (exp/i If' Th El)
           <- step If If'.
step/i2 : step (exp/i (exp/b true) Th El) Th.
step/i3 : step (exp/i (exp/b false) Th El) El.

does : exp -> type.
does/step : step E E' -> does E.
does/done : value E -> does E.

progress/plus/3 : {N}{M} does (exp/+ (exp/n N) (exp/n M)) -> type.
%mode progress/plus/3 +N +M -D.

- : progress/plus/3 z M (does/step (step/+3 plus/z)).
- : progress/plus/3 (s N) M (does/step (step/+3 (plus/s P)))
     <- progress/plus/3 N M (does/step (step/+3 P)).

%worlds () (progress/plus/3 _ _ _).
%total (N) (progress/plus/3 N _ _).

progress/plus : of N ty/nat -> of M ty/nat
                 -> does N -> does M -> does (exp/+ N M) -> type.
%mode progress/plus +O +O' +N +M -D.

- : progress/plus O O' (does/step S) M (does/step (step/+1 S)).
- : progress/plus O O' (does/done V) (does/step S) (does/step (step/+2 S V)).
- : progress/plus O O' (does/done (value/n N)) (does/done (value/n M)) D
     <- progress/plus/3 N M D.

%worlds () (progress/plus _ _ _ _ _).
%total (N) (progress/plus _ _ N _  _).

progress/if : of I ty/bool -> of T Ty -> of E Ty' ->
              does I -> does (exp/i I T E) -> type.
%mode progress/if +OI +OT +OE +I -E.

- : progress/if OI OT OE (does/step S) (does/step (step/i1 S)).
- : progress/if OI OT OE (does/done (value/b true)) (does/step step/i2).
- : progress/if OI OT OE (does/done (value/b false)) (does/step step/i3).

%worlds () (progress/if _ _ _ _ _).
%total (T) (progress/if _ _ _ T _).

progress/let : of B Ty -> ({x : exp} of x Ty -> of (F x) Ty') ->
               does B -> does (exp/l B F) -> type.
%mode progress/let +OB +OF +DB -D.

- : progress/let OB OD (does/done V) (does/step (step/l2 V)).
- : progress/let OB OD (does/step S) (does/step (step/l1 S)).

%worlds () (progress/let _ _ _ _).
%total (T) (progress/let _ _ T _).

progress : of E T -> does E -> type.
%mode progress +E -S.

- : progress (of/n N) (does/done (value/n N)).
- : progress (of/b B) (does/done (value/b B)).
- : progress (of/+ (N : of NE ty/nat) M) D
     <- progress M MD
     <- progress N ND
     <- progress/plus N M ND MD D.
- : progress (of/i I T E) D
     <- progress I DI
     <- progress/if I T E DI D.
- : progress (of/l B F) D
     <- progress B DB
     <- progress/let B F DB D.

%worlds () (progress _ _).
%total (T) (progress T _).

pres : of E T -> step E E' -> of E' T -> type.
%mode pres +O +S -O'.

- : pres (of/+ L R) (step/+1 S) (of/+ L' R)
     <- pres L S L'.
- : pres (of/+ L R) (step/+2 S V) (of/+ L R')
     <- pres R S R'.
- : pres (of/+ L R) (step/+3 (P : plus N M E)) (of/n E).
- : pres (of/l L F) (step/l1 S) (of/l L' F)
     <- pres L S L'.
- : pres (of/l L F) (step/l2 (V : value E)) (F E L).
- : pres (of/i I T E) (step/i1 S) (of/i I' T E)
     <- pres I S I'.
- : pres (of/i I T E) step/i2 T.
- : pres (of/i I T E) step/i3 E.

%worlds () (pres _ _ _).
%total (T) (pres _ T _).