Summer school 2008:Encoding of System F

Syntax

Types:

%sort tp %.
%term arrow %pi tp %-> tp %-> tp %.
%term forall %pi (%pi tp %-> tp) %-> tp %.

Terms:

%sort tm %.
%term fn %pi tp %-> (%pi tm %-> tm) %-> tm %.
%term app %pi tm %-> tm %-> tm %.
%term tfn %pi (%pi tp %-> tm) %-> tm %.
%term tapp %pi tm %-> tp %-> tm %.

Static semantics

%sort of {_ tm} {_ tp} %.
%term of-fn %pi (of (fn T2 ([x tm] E x)) (arrow T2 T)) %<- ({x tm} {dx of x T2} of (E x) T) %.
%term of-app %pi (of (app E1 E2) T) %<- (of E1 (arrow T2 T)) %<- (of E2 T2) %.
%term of-tfn %pi (of (tfn ([u tp] E u)) (forall ([u tp] T u))) %<- ({u tp} of (E u) (T u)) %.
%term of-tapp %pi (of (tapp E T2) (T T2)) %<- (of E (forall ([u] T u))) %.

Dynamic semantics

%sort value {_ tm} %.
%term value-fn value (fn A E) %.
%term value-tfn value (tfn E) %.
%sort step {_ tm} {_ tm} %.
%term step-app-1 %pi (step (app E1 E2) (app E1' E2)) %<- (step E1 E1') %.
%term step-app-2 %pi (step (app V1 E2) (app V1 E2')) %<- (value V1) %<- (step E2 E2') %.
%term step-app-beta %pi (step (app (fn T2 ([x tm] E x)) E2) (E E2)) %<- (value E2) %.
%term step-tapp-1 %pi (step (tapp E1 T) (tapp E1' T)) %<- (step E1 E1') %.
%term step-tapp-beta step (tapp (tfn ([u tp] E u)) T2) (E T2) %.