将证明环境粘合在一起：以锁为特征的LF类型论的规范扩展
Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks
摘要：
我们提出了两个扩展的LF建设性类型论具有一元锁。锁是一个一元类型构造，它捕获对oracle的外部调用的效果。这样的调用是将不同的类型论和证明开发环境粘合在一起的基本工具。可以调用oracle来检查约束是否成立，或者提供合适的见证。这些系统以CMU学校开发的规范风格呈现。第一个系统，CLLFP，是系统LLFP的规范版本，由作者早先提出。第二个系统，CLLFP？，其特征在于可以调用oracle来获得满足给定约束的见证。我们讨论了Fitch-Prawitz集理论的编码，按值调用算法和轻型线性逻辑系统。最后，我们展示了如何使用Fitch-Prawitz集合理论来定义一个类型系统，该类型系统精确地类型化强规范化项。
英文摘要：
We present two extensions of the LF Constructive Type Theory featuring monadic locks. A lock is a monadic type construct that captures the effect of an external call to an oracle. Such calls are the basic tool for gluing together diverse Type Theories and proof development environments. The oracle can be invoked either to check that a constraint holds or to provide a suitable witness. The systems are presented in the canonical style developed by the CMU School. The first system, CLLFP, is the canonical version of the system LLFP, presented earlier by the authors. The second system, CLLFP?, features the possibility of invoking the oracle to obtain a witness satisfying a given constraint. We discuss encodings of Fitch-Prawitz Set theory, call-by-value lambda-calculi, and systems of Light Linear Logic. Finally, we show how to use Fitch-Prawitz Set Theory to define a type system that types precisely the strongly normalizing terms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
