Denotation of contextual modal type theory (CMTT): Syntax and meta-programming

作者：Gabbay Murdoch J^*; Nanevski Aleksandar

来源：Journal of Applied Logic, 2013, 11(1): 1-29.

DOI：10.1016/j.jal.2012.07.002

• S4 modal logic
• Curry-Howard correspondence
• Contextual modal type theory
• Meta-programming
• Higher-order logic
• Syntax

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 %26apos;closed syntax of the calculus%26apos;. This lambda-calculus is called modal type theory-this is the basic case of a more general contextual modal type theory, or CMTT. %26lt;br%26gt;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.

• 出版日期2013-3