证明带有控制算子的系统 F 的求值终止性
编程语言
2013-09-06 v1 计算机科学中的逻辑
摘要
我们提出了带有控制算子的系统 F 在归约语义（即具有显式求值上下文表示的小步操作语义）中求值终止性的新证明。我们引入了基于可归约性候选（reducibility candidates）的 Girard 证明方法的修改版本，其中可归约性谓词是根据归约语义格式定义在值和求值上下文上的。我们针对中止型控制算子（callcc）和 delimited-control 算子（shift 和 reset）进行了处理，并为它们引入了新的多态类型系统；同时考虑了按值调用和按名调用两种求值策略。
引用
@article{arxiv.1309.1261,
title = {Proving termination of evaluation for System F with control operators},
author = {Małgorzata Biernacka and Dariusz Biernacki and Sergueï Lenglet and Marek Materzok},
journal= {arXiv preprint arXiv:1309.1261},
year = {2013}
}
备注
In Proceedings COS 2013, arXiv:1309.0924