Explicit Substitutions for Contextual Type Theory

Andreas Abel
(Ludwig-Maximilians-University )
Brigitte Pientka
(McGill University)

In this paper, we present an explicit substitution calculus which distinguishes between ordinary bound variables and meta-variables. Its typing discipline is derived from contextual modal type theory. We first present a dependently typed lambda calculus with explicit substitutions for ordinary variables and explicit meta-substitutions for meta-variables. We then present a weak head normalization procedure which performs both substitutions lazily and in a single pass thereby combining substitution walks for the two different classes of variables. Finally, we describe a bidirectional type checking algorithm which uses weak head normalization and prove soundness.

In Karl Crary and Marino Miculan: Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2010), Edinburgh, UK, 14th July 2010, Electronic Proceedings in Theoretical Computer Science 34, pp. 5–20.
Published: 11th September 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.34.3 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org