Denotation of contextual modal type theory (CMTT): Syntax and meta-programming |
| |
Authors: | Murdoch J Gabbay Aleksandar Nanevski |
| |
Institution: | 1. School of Mathematical and Computer Sciences, Heriot–Watt University, Riccarton Edinburgh, EH14 4AS, United Kingdom;2. IMDEA Software, Facultad de Informática (UPM), Campus Montegancedo, 28660 Boadilla del Monte, Madrid, Spain |
| |
Abstract: | The modal logic S4 can be used via a Curry–Howard style correspondence to obtain a λ-calculus. Modal (boxed) types are intuitively interpreted as ‘closed syntax of the calculus’. This λ-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. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|