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: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:50 - 18:00
TypesResearch Papers at Aurora Borealis
Chair(s): Richard A. EisenbergBryn Mawr College, USA
16:50
23m
Talk
Simple Noninterference from Parametricity
Research Papers
Maximilian AlgehedChalmers University of Technology, Sweden, Jean-Philippe BernardyUniversity of Gothenburg
17:13
23m
Talk
Selective Applicative Functors
Research Papers
Andrey MokhovNewcastle University, UK, Georgy LukyanovNewcastle University, UK, Simon MarlowFacebook, Jeremie DiminoJane Street Europe
Link to publication
17:36
23m
Talk
Coherence of Type Class Resolution
Research Papers
Gert-Jan BottuKU Leuven, Ningning XieThe University of Hong Kong, Koar MarntirosianKU Leuven, Tom SchrijversKU Leuven