Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Mon 19 Aug 2019 16:50 - 17:13 at Aurora Borealis - Types Chair(s): Richard A. Eisenberg

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 Aug
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:50 - 18:00: Research Papers - Types at Aurora Borealis
Chair(s): Richard A. EisenbergBryn Mawr College, USA
icfp-2019-papers16:50 - 17:13
Maximilian AlgehedChalmers University of Technology, Sweden, Jean-Philippe BernardyUniversity of Gothenburg
icfp-2019-papers17:13 - 17:36
Andrey MokhovNewcastle University, UK, Georgy LukyanovNewcastle University, UK, Simon MarlowFacebook, Jeremie DiminoJane Street Europe
Link to publication
icfp-2019-papers17:36 - 18:00
Gert-Jan BottuKU Leuven, Ningning XieThe University of Hong Kong, Klara MardirosianKU Leuven, Tom SchrijversKU Leuven