一句话：提出支持递归类型、存在类型、标签多态与不可谓词多态的信息流控制类型系统，用逻辑关系与模态最弱前置条件证明终止不敏感非干扰。
本文面向带高阶状态的高阶语言，提出表达力强的信息流控制类型系统，支持递归类型、存在类型、标签多态与不可谓词多态。为证明良类型程序满足终止不敏感非干扰，作者在 Iris 程序逻辑之上构建逻辑关系语义模型；为处理终止不敏感，提出语言无关的模态最弱前置条件理论。该语义方法支持将语法良类型与语法不良类型但语义健全的组件进行组合式集成，并通过多个实例展示其灵活性。全部理论与示例在 Coq 中机械化。
We present an expressive information-flow control type system with recursive types, existential types, label polymorphism, and impredicative type polymorphism for a higher-order programming language with higher-order state. We give a novel semantic model of this type system and show that well-typed programs satisfy termination-insensitive noninterference. Our semantic approach supports compositional integration of syntactically well-typed and syntactically ill-typed---but semantically sound---components, which we demonstrate through several interesting examples. We define our model using logical relations on top of the Iris program logic framework; to capture termination-insensitivity, we develop a novel language-agnostic theory of Modal Weakest Preconditions. We formalize all of our theory and examples in the Coq proof assistant.
@article{paperbot1173,
title = {Mechanized logical relations for termination-insensitive noninterference},
author = {Simon Oddershede Gregersen and Johan Bay and Amin Timany and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434291}
}