Contextual Modal Type Theory with Polymorphic Contexts

<jats:title>Abstract</jats:title><jats:p>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 <jats:italic>contextual modal type theory</jats:italic>, which has modal types with fine-grained information on free variables: modal types are explicitly indexed by <jats:italic>contexts</jats:italic>—the types of all free variables in code values.</jats:p><jats:p>This paper presents <jats:inline-formula><jats:alternatives><jats:tex-math>$$\lambda _{\forall []}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mi>λ</mml:mi> <mml:mrow> <mml:mo>∀</mml:mo> <mml:mo>[</mml:mo> <mml:mo>]</mml:mo> </mml:mrow> </mml:msub> </mml:math></jats:alternatives></jats:inline-formula>, a novel extension of contextual modal type theory with <jats:italic>parametric polymorphism over contexts</jats:italic>. Such an extension has been studied in the literature but, unlike earlier proposals, <jats:inline-formula><jats:alternatives><jats:tex-math>$$\lambda _{\forall []}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mi>λ</mml:mi> <mml:mrow> <mml:mo>∀</mml:mo> <mml:mo>[</mml:mo> <mml:mo>]</mml:mo> </mml:mrow> </mml:msub> </mml:math></jats:alternatives></jats:inline-formula> is more general in that it allows multiple occurrence of context variables in a single context. We formalize <jats:inline-formula><jats:alternatives><jats:tex-math>$$\lambda _{\forall []}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mi>λ</mml:mi> <mml:mrow> <mml:mo>∀</mml:mo> <mml:mo>[</mml:mo> <mml:mo>]</mml:mo> </mml:mrow> </mml:msub> </mml:math></jats:alternatives></jats:inline-formula> with its type system and operational semantics given by <jats:inline-formula><jats:alternatives><jats:tex-math>$$\beta $$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>β</mml:mi> </mml:math></jats:alternatives></jats:inline-formula>-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’ <jats:inline-formula><jats:alternatives><jats:tex-math>$$\lambda _{\bigcirc }$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mi>λ</mml:mi> <mml:mo>◯</mml:mo> </mml:msub> </mml:math></jats:alternatives></jats:inline-formula>, which is based on linear-time temporal logic, to <jats:inline-formula><jats:alternatives><jats:tex-math>$$\lambda _{\forall []}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mi>λ</mml:mi> <mml:mrow> <mml:mo>∀</mml:mo> <mml:mo>[</mml:mo> <mml:mo>]</mml:mo> </mml:mrow> </mml:msub> </mml:math></jats:alternatives></jats:inline-formula> .</jats:p>