[TYPES] Paper: "Contextual Modal Type Theory"

[Brigitte Pientka]

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

        http://www.cs.cmu.edu/~fp/papers/cmtt05.pdf

As always, comments are welcome.

-- Aleks Nanevski, Frank Pfenning and Brigitte Pientka