...
It is known that access control logics can be given a clear semantics using a realizability. Abadi has written about this as well as several other authors, and there is a mapping of Abadi's particular logic, CDD, into system F. However, in his paper Variations in Access Control Logic from 2008, he does not employ realizability. I will interpret his results using evidence semantics because the proofs can be made simpler, they suggest implementation ideas, and because his results illustrate a principle that Mark and I advance: the natural logic of distributed computing is intuitionistic.
...