Polymorphic Context for Contextual Modality
share
Through the Curry-Howard isomorphism between logics and calculi, necessity modality in logic is interpreted as types representing program code. Particularly, , which was proposed in influential work by Davies, and its successors have been widely used as a logical foundation for syntactic meta-programming. However, it is less known how to extend calculi based on modal type theory to handle more practical operations including manipulation of variable binding structures. This paper constructs such a modal type theory in two steps. First, we reconstruct contextual modal type theory by Nanevski, et al. as a Fitch-style system, which introduces hypothetical judgment with hierarchical context. The resulting type theory, contextual modal type theory , is generalized to accommodate not only S4 but also K, T, and K4 modalities, and proven to enjoy many desired properties. Second, we extend with polymorphic context, which is an internalization of contextual weakening, to obtain a novel modal type theory . Despite the fact that it came from observation in logic, polymorphic context allows both binding manipulation and hygienic code generation. We claim this by showing a sound translation from to .
READ FULL TEXT