University of Cambridge > > Computer Laboratory Programming Research Group Seminar > Denotation of Contextual Modal Type theory

Denotation of Contextual Modal Type theory

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Dominic Orchard.

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 (

This talk is part of the Computer Laboratory Programming Research Group Seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity