miniml-lists-value-soundness.elf

% Jesper Louis Andersen
% This is a proof of value soundness of miniml+lists

vs : %{{E:exp} {V:exp}}% eval E V -> value V -> type.
%mode vs +EP -VP.

vs_z : vs ev_z val_z.

vs_s : vs (ev_s EP) (val_s VP)
	<- vs EP VP.

vs_case_z: vs (ev_case_z EP2 EP1) VP2
	    <- vs EP2 VP2.

vs_case_s: vs (ev_case_s EP2 EP1) VP2
	    <- vs EP2 VP2.

vs_lam : vs ev_lam val_lam.

vs_app : vs (ev_app EP3 EP2 EP1) VP3
	  <- vs EP3 VP3.

vs_fix : vs (ev_fix EP) VP
	  <- vs EP VP.

% --- Adds

vs_nil : vs ev_nil val_nil.
vs_cons : vs (ev_cons EP2 EP1) (val_cons P2 P1)
	   <- vs EP2 P2
	   <- vs EP1 P1.

vs_lcase_nil : vs (ev_lcase_nil D2 D1) P
		<- vs D2 P.
vs_lcase_cons : vs (ev_lcase_cons D2 D1) P
		 <- vs D2 P.

%worlds () (vs _ _).
%total VP (vs VP _).