本文重新审视参数性与非干扰性之间的联系。作者在构造演算（Calculus of Constructions）中研究依赖核心演算（Dependency Core Calculus）的一个 polyvariant 变体，并证明其非干扰性。证明是模块化的：它利用构造演算的参数性，以及用存在类型编码数据抽象，从而从参数性推出简单且易于理解的非干扰性证明。所有贡献均已在 Agda 证明助手中机械化。
问题
研究参数性与非干扰性之间的联系，并证明依赖核心演算的 polyvariant 变体满足非干扰性。
方法
在构造演算中形式化该变体，模块化地利用参数性和存在类型编码的数据抽象来构造非干扰性证明。
评估
所有定义与证明均在 Agda 证明助手中机械化验证。
原文摘要（Abstract）
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.
@article{paperbot595,
title = {Simple noninterference from parametricity},
author = {Maximilian Algehed and Jean-Philippe Bernardy},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341693}
}