局部无名置换类型
编程语言
2017-10-25 v1 计算机科学中的逻辑
摘要
我们定义了“局部无名置换类型”，它将Nominal Isabelle中使用的置换类型与局部无名表示相融合。我们表明，在形式化那些绑定名在执行过程中可能变为自由名(“挤出”，extrusion)的编程语言(在进程演算中常见)时，这种组合特别有用。它从Nominal方法继承了置换与支撑(support)的通用定义及相关引理，并从局部无名方法继承了贴近纸笔证明的能力。我们解释了如何在此设定中使用余有限量化(cofinite quantification)，说明了为何相较于无非挤出语言，此处关于重命名的推理更为重要，并给出了关于无限支撑的结果，这是推理可数选择时必需的。
引用
@article{arxiv.1710.08444,
title = {Locally Nameless Permutation Types},
author = {Edsko de Vries and Vasileios Koutavas},
journal= {arXiv preprint arXiv:1710.08444},
year = {2017}
}
备注
Coq code in ancillary files