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 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:50 - 18:00
|Simple Noninterference from Parametricity|
|Selective Applicative Functors|
Andrey Mokhov Newcastle University, UK, Georgy Lukyanov Newcastle University, UK, Simon Marlow Facebook, Jeremie Dimino Jane Street EuropeLink to publication
|Coherence of Type Class Resolution|