[isabelle] New AFP entry: Possibilistic Noninterference

Possibilistic Noninterference
Andrei Popescu and Johannes Hölzl

We formalize a wide variety of Volpano/Smith-style noninterference notions for a
while language with parallel composition. We systematize and classify these
notions according to compositionality w.r.t. the language constructs.
Compositionality yields sound syntactic criteria (a.k.a. type systems) in a
uniform way.

An article http://www21.in.tum.de/~nipkow/pubs/cpp12.html about these proofs is
published in the proceedings of the conference Certified Programs and Proofs 2012


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.