Parametricity Semantics of Symmetric Noninterference Seminars/Workshops

Abstract

Informally, two program phrases do not interfere if the execution of one program phrase doesn't affect that of the other. This notion of interference (and its opposite, noninterference) appears in several different fields of computer science including code optimization and formal programming logic. The approaches to understanding noninterference have been categorized into two groups: asymmetric interpretation and symmetric one. Even though there have been significant achievements in asymmetric interpretation, the existing work on the symmetric interpretation is not as satisfactory. In this talk, I'll talk about our work on the symmetric interpretation of noninterference in parametricity semantics of Idealized Algol, which improves upon existing work in that our model validates noninterference decomposition rule. Our work uses the idea from sheaf theory, more accurately our extension of it to parametricity theory, which helps to analyze semantics more closely so as to define more proper notion of noninterference.
(joint work with Uday S. Reddy in University of Birmingham)