Summer school 2008:Encoding of System F

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.
Summer school 2008
Previous: Exercises 2


Syntax

Types:

tp : type.  

arrow : tp -> tp -> tp.
forall : (tp -> tp) -> tp.

Terms:

tm : type. 

fn : tp -> (tm -> tm) -> tm.
app : tm -> tm -> tm.

tfn : (tp -> tm) -> tm.
tapp : tm -> tp -> tm.

Static semantics

of : tm -> tp -> type.

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

Dynamic semantics

value    : tm -> type.
value-fn : value (fn A E).
value-tfn : value (tfn E).


step : tm -> tm -> type.

step-app-1 : step (app E1 E2) (app E1' E2)
		<- step E1 E1'.
step-app-2 : step (app V1 E2) (app V1 E2')
		<- value V1
		<- step E2 E2'.
step-app-beta : step (app (fn T2 ([x:tm] (E x))) E2) (E E2)
		   <- value E2.
step-tapp-1 : step (tapp E1 T) (tapp E1' T)
		 <- step E1 E1'.
step-tapp-beta : step (tapp (tfn ([u:tp] E u)) T2) (E T2).
Summer school 2008
Previous: Exercises 2