局部精化类型推导
编程语言
2017-06-27 v1
摘要
我们引入了用于局部精化类型推导的 Fusion 算法，产生了一种新的基于 SMT 的方法，用于验证具有多态数据类型和高阶函数的程序。Fusion 非常简洁，因为程序员只需为（外部导出的）顶层函数和具有循环（递归）依赖的位置编写签名，之后 Fusion 就能可预测地为所有中间项合成最精确的精化类型（可在可判定的精化逻辑中表示），从而在没有误报的情况下检查程序。我们实现了 Fusion 并在 LiquidHaskell 套件的基准测试上进行了评估，总计约 12KLOC。Fusion 检查现有的安全基准测试套件所需的模板数量约为以前的一半，且速度快了近 2 倍。在一组新的定理证明基准测试中，Fusion 的速度快了 10 到 50 倍，并且通过合成最精确的类型，避免了误报，使验证成为可能。
引用
@article{arxiv.1706.08007,
title = {Local Refinement Typing},
author = {Benjamin Cosman and Ranjit Jhala},
journal= {arXiv preprint arXiv:1706.08007},
year = {2017}
}