Simple noninterference from parametricity
Simple noninterference from parametricity
复制标题
参数化的简单无干扰
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Jean
中科院分区：
文献类型：
--
作者：
Maximilian Algehed;Jean
在本文中，我们重新审视参数化和无干扰之间的联系。我们的主要贡献是证明了构造微积分中依赖核心微积分的多变量变体的无干扰性。证明是模块化的：它利用构造演算的参数性以及使用存在类型的数据抽象编码。这种观点提出了参数化不干扰的简单且易于理解的证明。我们所有的贡献都已在 Agda 证明助手中机械化。
In this paper we revisit the connection between parametricity and noninterference. Our primary contribution is a proof of noninterference for a polyvariant variation of the Dependency Core Calculus of in the Calculus of Constructions. The proof is modular: it leverages parametricity for the Calculus of Constructions and the encoding of data abstraction using existential types. This perspective gives rise to simple and understandable proofs of noninterference from parametricity. All our contributions have been mechanised in the Agda proof assistant.