Towards a type theory of contexts

ABSTRACT

At the 2003 Merlin workshop, we presented an initial report on providing a logical basis for the understanding of meta-variables. Our calculus rests on a contextual modality that is intrinsically connected to explicit substitutions, but does not provide a means for quantifying over substitutions or abstracting over contexts. In this talk we give a progress report on our attempts to obtain a modal type theory that integrates variables ranging over substitutions and contexts without losing its logical interpretation. This is joint work with Brigitte Pientka (McGill University, Canada) and Aleksandar Nanevski (Harvard University, USA).