Denotation of syntax and metaprogramming in contextual modal type theory (CMTT)

TL;DR

This paper develops a denotational semantics for the contextual modal type theory (CMTT), interpreting modal types as closed syntax, and uses this to establish properties of the system.

Contribution

It provides the first denotational semantics for CMTT, interpreting modal types as closed syntax and proving system properties using this semantics.

Findings

Successfully defines denotational semantics for CMTT

Interprets modal types as closed syntax

Proves properties of CMTT using the semantics

Abstract

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.