一句话：研究如何调和信息流控制中的非干涉与渐进类型，以恢复动态渐进保证。
本文关注渐进类型系统中动态渐进保证与信息流控制非干涉之间的冲突。动态渐进保证要求放宽类型标注不会任意改变程序行为，但已有工作指出，对信息流控制的渐进类型系统而言该保证不成立；例如 Toro 等人的 GSLRef 为保证非干涉不得不放弃动态渐进保证。论文以调和这两个目标为核心问题，标题表明其试图在渐进类型框架下重新处理非干涉，使信息流安全与渐进保证能够共存。摘要仅给出问题背景，未展开具体类型规则、语义或证明方法，也未说明评估结果，因此其技术路线与关键结论需参见正文。
One of the standard correctness criteria for gradual typing is the dynamic gradual guarantee, which ensures that loosening type annotations in a program does not affect its behavior in arbitrary ways. Though natural, prior work has pointed out that the guarantee does not hold of any gradual type system for information-flow control. Toro et al.'s GSLRef language, for example, had to abandon it to validate noninterference.
DOI 原文 ·
@inproceedings{paperbot5537,
title = {Reconciling noninterference and gradual typing},
author = {Arthur Azevedo de Amorim and Matt Fredrikson and Limin Jia},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394778}
}