论文标题
动态IFC定理免费！
Dynamic IFC Theorems for Free!
论文作者
论文摘要
我们表明，可以“自由”获得非干扰和透明度，即动态IFC库的关键音质定理，作为类型抽象的更通用参数定理的直接后果。这使我们可以为动态的IFC库（例如刻面值和lio）提供非常简短的声音证明。即使在类型抽象方面，即使完全机械化了图书馆的AGDA实施，我们的证明也保持不足。
We show that noninterference and transparency, the key soundness theorems for dynamic IFC libraries, can be obtained "for free", as direct consequences of the more general parametricity theorem of type abstraction. This allows us to give very short soundness proofs for dynamic IFC libraries such as faceted values and LIO. Our proofs stay short even when fully mechanized for Agda implementations of the libraries in terms of type abstraction.
