有界精化类型
编程语言
2015-07-03 v1 软件工程
摘要
我们提出一种用于精化类型的有界量化概念，并展示其如何通过用于以下方面的类型组合子来扩展精化类型化的表达能力：(1) 关系代数与安全数据库访问，(2) 配备用于分支和循环的组合子的状态转换器单子中的Floyd-Hoare逻辑，以及 (3) 使用上述方法实现追踪能力与资源使用的精化IO单子。这种表达能力的飞跃通过向“ghost”函数的翻译实现，使我们得以保留基于SMT的自动化可判定检查与推断，这正是精化类型化在实践中有效的关键。
引用
@article{arxiv.1507.00385,
title = {Bounded Refinement Types},
author = {Niki Vazou and Alexander Bakst and Ranjit Jhala},
journal= {arXiv preprint arXiv:1507.00385},
year = {2015}
}
备注
14 pages, International Conference on Functional Programming, ICFP 2015