Nanevski in his PhD thesis introduced and studied Contextual Modal Theory Theory. This is a lambda-calculus based via the Curry-Howard correspondence on an extension of the modal logic S4 with multiple modalities, one for each variable. The application is to meta-programming, where the intuitive denotation of Box A is “syntax of type A”.

The language itself is pretty, and we developed a denotational semantics for this which is quite attractive and displays some interesting properties. I will give a tour of the system and discuss future work. The associated journal paper on “Denotations of CMTT” is online.