Cocon：上下文类型论中的计算
Cocon: Computation in Contextual Type Theory
摘要：
我们描述了一个马丁-洛夫风格依赖的类型论，称为Cocon，它允许我们混合的内涵函数空间，用于表示高阶抽象语法（HOAS）树与扩展函数空间，描述（递归）计算。我们使用上下文模态类型在HOAS表示和计算之间进行调解。我们的类型论还支持无限层次的宇宙，因此支持类型级计算--从而提供元编程和（小规模）反射。我们的主要贡献是为Cocon开发了一个Kripke风格的模型，使我们能够证明正常化。从规范化的证明，我们得到的主题减少和一致性。我们的工作为将逻辑框架方法纳入Agda等系统奠定了基础，并弥合了这两个世界之间的长期差距。
英文摘要：
We describe a Martin-Löf style dependent type theory, called Cocon, that allows us to mix the intensional function space that is used to represent higher-order abstract syntax (HOAS) trees with the extensional function space that describes (recursive) computations. We mediate between HOAS representations and computations using contextual modal types. Our type theory also supports an infinite hierarchy of universes and hence supports type-level computation -- thereby providing metaprogramming and (small-scale) reflection. Our main contribution is the development of a Kripke-style model for Cocon that allows us to prove normalization. From the normalization proof, we derive subject reduction and consistency. Our work lays the foundation to incorporate the methodology of logical frameworks into systems such as Agda and bridges the longstanding gap between these two worlds.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
