约束逻辑程序的类型化
编程语言
2009-09-29 v1
摘要
我们提出了一种具有参数多态性和子类型的规范性类型系统，用于约束逻辑程序。该类型系统的目的是在静态阶段检测编程错误。得益于子类型的灵活性，它为约束逻辑程序和模块引入了类型规范，同时保持了在约束域之间执行常规强制类型转换以及对元编程谓词进行类型化的能力。主体归约性质表达了规范性类型系统相对于执行模型的一致性：如果一个程序是“良类型”的，那么从“良类型”目标出发的所有推导依然是“良类型”的。我们针对仅通过约束累积进行的约束编程抽象执行模型，以及带有类型约束的替换的扩充执行模型，证明了该性质。我们描述了用于类型检查和类型推断的系统实现。我们报告了对 ISO-Prolog、Sicstus Prolog 的（约束）库以及其他 Prolog 程序进行类型检查的实验结果。
引用
@article{arxiv.cs/0405100,
title = {Typing constraint logic programs},
author = {Francois Fages and Emmanuel Coquery},
journal= {arXiv preprint arXiv:cs/0405100},
year = {2009}
}
备注
Appeared in Theory and Practice of Logic Programming, vol. 1, no. 6, 2001