================================================= =================== LANG0 ======================= ================================================= differences between lang0 and capability calculus: - major: - general "resources", not regions (no region annotations) (newrgn, freergn, region ops --> new, free, use) - static concepts only (omit r, heap, heap types) - omit recursion - minor (for neatness, conciseness): - limit (C,t1,...,tn) to (C,t) - limit to - split all[D].(C,t)->0 into pieces - omit int type, integer ops - require kind annotation on c misc. notational differences ================================================= ================== SYNTAX ======================= ================================================= k = type | res | cap b = A | t | c t = A | A handle | all A:k.t | (c,t)->0 | | _t _t = all A<=c.t c = A | {} | {A p} | c1+c2 | /c p = ~ | + d = . | d,A:k | d,A<=c g = . | g,x:t v = x | v[b:k] h = \A:k.h | \(c,x:t).e | | _h _h = \A<=c.h l = x=v | x=h | x=v.n | new A,x | free v | use v e = let l in e | v1 v2 | halt ================================================= ================= SEMANTICS ===================== ================================================= d |- . d |- d' ----------- (A not in Dom(d,d')) d |- d',A:k d |- d' d,d' |- c:cap ------------- (A not in Dom(d,d')) d |- d',A<=c ================================================= d |- . d |- g d |- t:type ----------- (x not in Dom(g)) d |- g,x:t ================================================= ...,A:k,... |- A:k ...,A<=c,... |- A:cap d |- A:res ------------------ d |- A handle:type d |- t1:type d |- t2:type ----------------- d |- :type d,A:k |- t:type ------------------- (A not in Dom(d)) d |- all A:k.t:type d |- c:cap d,A<=c |- t:type -------------------- (A not in Dom(d)) d |- all A<=c.t:type d |- t:type d |- c:cap ------------------ d |- (c,t)->0:type d |- {}:cap d |- A:res -------------- d |- {A p}:cap d |- c1:cap d |- c2:cap -------------- d |- c1+c2:cap d |- c:cap ----------- d |- /c:cap ================================================= /* probably not necessary d |- . = . d |- d1 = d2 ------------------- (A not in Dom(d,d1)) d | d1,A:k = d2,A:k d |- d1 = d2 d,d1 |- c1 = c2:cap ---------------------------- (A not in Dom(d,d1)) d |- d1,A<=c1 = d1,A<=c2:cap */ ================================================= d |- b:k ------------ d |- b = b:k d |- b2 = b1:k -------------- d |- b1 = b2:k d |- b1 = b2:k d |- b2 = b3:k -------------- d |- b1 = b3:k d |- c1 = c1':k d |- c2 = c2':k ---------------------- where k = cap d |- c1+c2 = c1'+c2':k d |- c1 = c1':cap ------------------- d |- /c1 = /c1':cap d |- c:k --------------- where k = cap d |- {}+c = c:k d |- c1:k d |- c2:k -------------------- where k = cap d |- c1+c2 = c2+c1:k d |- c1:k d |- c2:k d |- c3:k ------------------------------ where k = cap d |- (c1+c2)+c3 = c1+(c2+c3):k d |- c:cap ------------------- d |- /c = /c+/c:cap d |- /{} = {}:cap d |- A:res --------------------- d |- /{A~} = {A+}:cap d |- c:cap ----------------- d |- //c = /c:cap d |- c1:cap d |- c2:cap --------------------------- d |- /(c1+c2) = /c1+/c2:cap ================================================= d |- c1 = c2:k -------------- where k = cap d |- c1 <= c2 d |- c1 <= c2 d |- c2 <= c3 ------------- d |- c1 <= c3 d |- c1 <= c1' d |- c2 <= c2' --------------------- d |- c1+c2 <= c1'+c2' d |- c <= c' -------------- d |- /c <= /c' ...,A<=c,... |- A<=c d |- c:cap ------------ d |- c <= /c d |- c:cap ------------ (optional) d |- c <= {} ================================================= d |- t1 = t1':type d |- t2 = t2':type ----------------------------- d |- = :type d,A:k |- t = t':type -------------------------------- (A not in Dom(d)) d |- all A:k.t = all A:k.t':type d |- c = c':cap d,A<=c |- t = t':type ----------------------------------- (A not in Dom(d)) d |- all A<=c.t = all A<=c'.t':type d |- t = t':type d |- c = c':cap ------------------------------- d |- (c,t)->0 = (c',t')->0:type ================================================= d,A:k;g |- h:t ------------------------ (A not in Dom(d)) d;g |- \A:k.h: all A:k.t d |- c:cap d,A<=c;g |- h:t -------------------------- (A not in Dom(d)) d;g |- \A<=c.h: all A<=c.t d |- c:cap d |- t:type d;g,x:t;c |- e --------------------------- (x not in Dom(g)) d;g |- \(c,x:t).e: (c,t)->0 d;g |- v1: t1 d;g |- v2: t2 ----------------------- d;g |- : d;g |- h: t' d |- t' = t:type ---------------- d;g |- h: t ================================================= d;...,x:t,... |- x: t d;g |- v: all A:k.t d |- b:k ---------------------- d;g |- v[b:k]: [A<-b]t d;g |- v: all A<=c'.t d |- c <= c' ------------------------ d;g |- v[c:cap]: [A<-c]t d;g |- v: t' d |- t' = t:type ---------------- d;g |- v: t ================================================= d;g |- v:t -------------------------- (x not in Dom(g)) d;g;c |- x=v ==> d;g,x:t;c d;g |- h:t -------------------------- (x not in Dom(g)) d;g;c |- x=h ==> d;g,x:t;c d;g |- v: ------------------------------ (x not in Dom(g) and 1<=n<=2) d;g;c |- x=v.n ==> d;g,x:t_n;c d;g;c |- new A,x ==> d,A:res;g,x:A handle;c+{A~} (A not in Dom(d) and x not in Dom(g)) d;g |- v: A handle d |- c = c'+{A~}:cap -------------------------- d;g;c |- free v ==> d;g;c' d;g |- v: A handle d |- c <= c'+{A+} ------------------------ d;g;c |- use v ==> d;g;c ================================================= d;g;c |- l ==> d';g';c' d';g';c' |- e ----------------------- d;g;c |- let l in e d;g |- v1: (c',t)->0 d;g |- v2: t d |- c <= c' -------------------- d;g;c |- v1 v2 d |- c = {}:cap --------------- d;g;c |- halt ================================================= =================== LEMMAS ====================== ================================================= Language lemmas: - if |- d and d |- g and d;g |- v:t then d |- t:type - if |- d and d |- g and d;g |- h:t then d |- t:type