In this paper we revisit the connection between parametricity and noninterference. Our primary contribution is a proof of noninterference for a shallow embedding of a polyvariant variation of the Dependency Core Calculus of Abadi et al.  in the Calculus of Constructions [Coquand and Huet 1988] based entirely on parametricity. The proof is based on the notion of encoding data abstraction using existential types of Cardelli and Wegner . Our contributions are made in the context of dependent types and parametricity for Pure Type Systems due to Bernardy et al. . This perspective gives rise to simple and understandable proofs of noninterference from parametricity. All our contributions have been mechanised in the Agda proof assistant [Norell 2007].
Mon 19 Aug
|16:50 - 17:13|
|17:13 - 17:36|
Andrey MokhovNewcastle University, UK, Georgy LukyanovNewcastle University, UK, Simon MarlowFacebook, Jeremie DiminoJane Street EuropeLink to publication
|17:36 - 18:00|