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. [1999] 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 [1985]. Our contributions are made in the context of dependent types and parametricity for Pure Type Systems due to Bernardy et al. [2012]. 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 | |||
16:50 23mTalk | Simple Noninterference from Parametricity Research Papers Maximilian Algehed Chalmers University of Technology, Sweden, Jean-Philippe Bernardy University of Gothenburg | ||
17:13 23mTalk | Selective Applicative Functors Research Papers Andrey Mokhov Newcastle University, UK, Georgy Lukyanov Newcastle University, UK, Simon Marlow Facebook, Jeremie Dimino Jane Street Europe Link to publication | ||
17:36 23mTalk | Coherence of Type Class Resolution Research Papers Gert-Jan Bottu KU Leuven, Ningning Xie University of Toronto, Koar Marntirosian KU Leuven, Tom Schrijvers KU Leuven | ||