上下文模态类型论（CMTT）中的语法表示和元编程
Denotation of syntax and metaprogramming in contextual modal type theory (CMTT)
摘要：
模态逻辑S4可以通过Curry-Howard风格的对应关系来使用，以获得一个模态演算。模态（盒装）类型被直观地解释为“演算的封闭语法”。这种模式演算被称为模态类型论--这是更一般的上下文模态类型论或CMTT的基本情况。CMTT从来没有被赋予一个指称语义，其中模态类型被赋予作为封闭语法的指称。我们展示了如何确实可以做到这一点，与扭曲。我们还利用这个表示证明了系统的一些性质。
英文摘要：
The modal logic S4 can be used via a Curry-Howard style correspondence to obtain a lambda-calculus. Modal (boxed) types are intuitively interpreted as `closed syntax of the calculus'. This lambda-calculus is called modal type theory --- this is the basic case of a more general contextual modal type theory, or CMTT. CMTT has never been given a denotational semantics in which modal types are given denotation as closed syntax. We show how this can indeed be done, with a twist. We also use the denotation to prove some properties of the system.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
