PRL Seminar for Friday Sept 23

Analyzing Access Control Logics Using Evidence Semantics

Presented by Robert Constable

It is known that access control logics can be given a clear semantics using 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.

...