Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
% 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 _).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment