PRL Seminar for Friday Sept 23
Presented by Robert Constable
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 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 implementaion ideas, and because his results illustrate a principle that Mark and I advance: the natural logic of distributed computing is intuitionistic.
...