# Contextual Modal Type Theory with Polymorphic Contexts

arXiv: https://arxiv.org/abs/1801.09225 · HTML: https://mlsanity.com/paper/1801.09225/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Jan 2018.

## Built on by (most cited first, 1 of 1)

- [STEM-POM: Evaluating Language Models Math-Symbol Reasoning in Document Parsing](https://mlsanity.com/paper/2411.00387/) (2024)

## Abstract (arXiv)

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[].