粘合证明环境：具有锁的LF类型理论的标准扩展
计算机科学中的逻辑
2015-07-30 v1
摘要
我们提出了具有单子锁(monadic locks)的LF构造类型理论(LF Constructive Type Theory)的两个扩展。锁是一种单子类型构造，捕获对预言机(oracle)外部调用的效应。此类调用是粘合不同种类类型理论与证明开发环境的基本工具。预言机可被调用以检查约束是否成立，或提供合适的见证(witness)。这些系统以CMU学派发展的标准风格给出。第一个系统CLLFP是作者早先提出的LLFP系统的标准版本。第二个系统CLLFP? 支持调用预言机以获得满足给定约束的见证。我们讨论了Fitch-Prawitz集合论、按值调用lambda演算以及轻线性逻辑系统的编码。最后，我们展示如何使用Fitch-Prawitz集合论来定义一个类型系统，该类型系统恰好对强规范化项进行类型指派。
引用
@article{arxiv.1507.08051,
title = {Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks},
author = {Furio Honsell and Luigi Liquori and Petar Maksimović and Ivan Scagnetto},
journal= {arXiv preprint arXiv:1507.08051},
year = {2015}
}
备注
In Proceedings LFMTP 2015, arXiv:1507.07597