=================================================
=================== CC/CCL ======================
=================================================

(this is exactly the capability calculus of Crary,Walker,Morrisett)

=================================================
================== SYNTAX =======================
=================================================

k = type | res | cap
b = A | t | r | c
t = A | int | r handle | all[d](C,t1...tn)->0 at r | <t1...tn> at r
r = A | q
c = A | {} | {r p} | c1+c2 | /c
p = ~ | +

d = . | d,A:k | d,A<=c
g = . | g,x:t
y = i1:t1...in:tn
z = q1:y1...qn:yn

v = x | n | q.i | handle(q)| v[b]
h = fix x[d](c,x1:t1,...,xn:tn).e | <v1...vn>
op = + | - | *
l = x=v | x=v1 op v2 | x=h at v | x=v.n | new A,x | free v
e = let l in e | if0 v then e2 else e3 | v(v1...vn) | halt v

w = i1->h1...in->hn
m = q1->w1...qn->wn

=================================================
================= 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
-----------
d |- g,x:t

=================================================

...,A:k,... |- A:k

d |- int:type

d |- r:res
------------------
d |- r handle:type

d |- q:res

d |- t1:type
...
d |- tn:type
d |- r:res
--------------------------
d |- <t1,...,tn> at r:type

d |- d'
d,d' |- t1:type
...
d,d' |- tn:type
d,d' |- c:cap
d |- r:res
------------------------------------
d |- all[d'](c,t1...tn)->0 at r:type

|- y1
...
|- yn
------------------
|- {q1:y1...qn:yn}

|- t1:type
...
|- tn:type
------------------
|- {i1:t1...in:tn}

...,A<=c,... |- A:cap

d |- {}:cap

d |- r:res
--------------
d |- {r p}:cap

d |- c1:cap
d |- c2:cap
--------------
d |- c1+c2:cap

d |- c:cap
-----------
d |- /c:cap

=================================================

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 = d2,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 |- t1=t1':type
...
d |- tn=tn':type
-----------------------------------------------
d |- <t1,...,tn> at r = <t1',...,tn'> at r:type

d'' |- d = d'
d'',d |- t1 = t1':type
...
d'',d |- tn = tn':type
d'',d |- c = c':cap
d |- r:res
---------------------------------------------------------------------
d'' |- all[d](c,t1...tn)->0 at r = all[d'](c',t1'...tn')->0 at r:type

=================================================

d |- d'
d,d' |- c:cap
d,d' |- t1:type
...
d,d' |- tn:type
d |- r:res
z;d,d';g,x:tx,x1:t1...xn:tn;c |- e
tx = all[d'](c,t1...tn)->0 at r
--------------------------------------------- (x,x1...xn not in dom(g))
z;d;g |- fix x[d'](c,x1:t1...xn:tn).e at r:tx

z;d;g |- v1:t1
...
z;d;g |- vn:tn
d |- r:res
--------------------------------------
z;d;g |- <v1...vn> at r:<t1...tn> at r

z;d;g |- h at r: t'
d |- t' = t:type
------------------
z;d;g |- h at r: t

=================================================

z;d;...,x:t,... |- x: t

z;d;g |- n:int

d |- <t1...tn> at q:type
--------------------------- (q not in dom(z))
z;d;g |- q.i:<t1...tn> at q

d |- all[d'](c,t1...tn)->0 at q:type
--------------------------------------- (q not in dom(z))
z;d;g |- q.i:all[d'](c,t1...tn)->0 at q

z;d;g |- q.i:z(q.i)

z;d;g |- handle(q):q handle

z;d;g |- v: all[A:k,d'](c,t1...tn)->0 at r
d |- b:k
-------------------------------------------------
z;d;g |- v[b]: [A<-b](all[d'](c,t1...tn)->0 at r)

z;d;g |- v: all[A<=c'',d'](c',t1...tn)->0 at r
d |- c <= c''
--------------------------------------------------
z;d;g |- v[c]: [A<-c](all[d'](c',t1...tn)->0 at r)

z;d;g |- v: t'
d |- t' = t:type
----------------
z;d;g |- v: t

=================================================

z;d;g |- v:t
---------------------------- (x not in dom(g))
z;d;g;c |- x=v ==> d;g,x:t;c

z;d;g |- v1:int
z;d;g |- v2:int
------------------------------------- (x not in dom(g))
z;d;g;c |- x=v1 op v2 ==> d;g,x:int;c

z;d;g |- v:r handle
z;d;g |- h at r:t
d |- c<=c'+{r+}
--------------------------------- (x not in dom(g))
z;d;g;c |- x=h at v ==> d;g,x:t;c

z;d;g |- v:<t0...tm-1> at r
d |- c<=c'+{r+}
------------------------------ (x not in dom(g) and 0<=n<m)
z;d;g;c |- x=v.n ==> d;g,x:tm;c

z;d;g;c |- newrgn A,x ==> d,A:res;g,x:A handle;c+{A~} (A not in dom(d) and x not in dom(g))

z;d;g |- v: r handle
d |- c = c'+{r~}:cap
-------------------------------
z;d;g;c |- freergn v ==> d;g;c'

=================================================

z;d;g;c |- l ==> d';g';c'
z;d';g';c' |- e
-----------------------
z;d;g;c |- let l in e

z;d;g |- v:int
z;d;g;c |- e2
z;d;g;c |- e3
--------------------------------
z;d;g;c |- if0 v then e2 else e3

z;d;g |- v: all[](c',t1...tn)->0 at r
z;d;g |- v1: t1
...
z;d;g |- vn: tn
d |- c<=c''+{r+}
d |- c <= c'
---------------------
z;d;g;c |- v(v1...vn)

z;d;g |- v:int
d |- c = {}:cap
-----------------
z;d;g;c |- halt v

=================================================

|- z
z |- w1 at q1:y1
...
z |- wn at qn:yn
z = q1:y1...qn:yn
--------------------
|- q1->w1...qn->wn:z

z;; |- h1 at q:t1
...
z;; |- hn at q:tn
-------------------------------------------
z |- {i1->h1...in->hn} at q:{i1:t1...in:tn}

|- c={q1 p1}+...+{qn pn}:cap
---------------------------- (all qi distinct)
q1:y1...qn:yn sat c

|- m:z
z sat c
z;;;c |- e
----------
|- (m,e)

=================================================