Contextual Modal Type Theory with Polymorphic Contexts

Modal types -- types that are derived from proof systems of modal logic -- have been studied as theoretical foundations of metaprogramming, where program code is manipulated as first-class values. In modal type systems, modality corresponds to a type constructor for code types and controls free variables and their types in code values. Nanevski et al. have proposed contextual modal type theory, which has modal types with fine-grained information on free variables: modal types are explicitly indexed by contexts -- the types of all free variables in code values. This paper presents λforall[], a novel extension of contextual modal type theory with parametric polymorphism over contexts. Such an extension has been studied in the literature but unlike earlier proposals, λforall[] is more general in that multiple parts of a single context can be abstracted. We formalize lamfb with its type system and operational semantics given by β-reduction and prove its basic properties including subject reduction, strong normalization, and confluence. Moreover, to demonstrate the expressive power of polymorphic contexts, we show a type-preserving embedding from a two-level fragment of Davies' λbigcirc, which is based on linear-time temporal logic, to λforall[].