  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.
