Building security directly into the code

[Christophe de Dinechin]

An interesting paper on building security directly into the code and verifying some of it at compile-time:

http://www.cs.cornell.edu/andru/papers/fabric-sosp09.pdf

Examples of code:

int {alice→bob} x;
int {alice→bob, charlie} y;
x=y;//OK:bob􏰅(bob∨charlie)
y = x; // Invalid
if (charlie actsfor bob) {
y = x; // OK: (bob ∨ charlie) 􏰅 bob
}

I did not read in details yet, but I wonder how you specify the actors themselves, e.g. alice and bob? Can they be the result of computations?