逐渐敏感性类型化
摘要：渐进型灵敏度类型：动态和静态结合 摘要:关于函数对其输入的敏感性的推理在各个领域都有着有趣的应用，如差分隐私。为了检查和强制敏感性，已经开发了几种方法，尤其是敏感性类型系统。在这些系统中，敏感性可以看作是类型和效果系统中的一种效果，这是最初由Gifford和Lucassen提出的。由于类型和效果系统可能会使某些有用的编程模式变得繁琐或过于保守，所以将渐进类型的优点引入到这些学科中有着重要价值，以便简化它们的采用。在这项工作中，我们提出了渐进灵敏度类型的动机、形式化和原型化。语言GSoul支持无限制的未知敏感性和以区间形式的有限不精确性。渐进灵敏度类型允许程序员在没有任何静态敏感性信息的情况下平滑地演化有类型的程序，向包含静态和动态敏感性检查的硬化程序过渡。特别是，我们展示了渐进灵敏度支持递归函数，这些函数的完全静态检查会过于保守，从而无缝地实现了精确的运行时敏感性检查。GSoul既满足渐进保证又满足敏感性类型的健全性，即度量保留。我们确定，一般来说，渐进度量保留与终止是不敏感的，而硬化规范可以实现对终止敏感的渐进度量保留。我们实现了一个提供渐进灵敏度类型交互式测试环境的原型。这项工作为将依赖于函数敏感性的其他类型学科（如差分隐私）以及其他定量类型推理技术逐渐化开门见山。
作者：Damian Arquez, Mat''ias Toro, ''Eric Tanter
论文ID：2308.02018
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-08-07