[TYPES] Paper: "Contextual Modal Type Theory"

Brigitte Pientka bpientka at cs.mcgill.ca
Fri Sep 30 07:48:07 EDT 2005

Dear Types readers,

We are pleased to announce the availability of our paper,
"Contextual Modal Type Theory". The intuitionistic modal logic of
necessity is based on the judgmental notion of categorical truth.  In
this paper we investigate the consequences of relativizing these
concepts to explicitly specified contexts.  We obtain contextual modal
logic and its type-theoretic analogue.

Contextual modal type theory provides an elegant, uniform foundation
for understanding meta-variables and explicit substitutions.
Moreover, it has applications to staged computation and run-time code
generation where it serves as a foundation to justify and reason about
open code.

The paper is available for download from


As always, comments are welcome.

-- Aleks Nanevski, Frank Pfenning and Brigitte Pientka

More information about the Types-list mailing list