Download Now Free registration required
In this paper, the authors present an explicit substitution calculus which distinguishes between ordinary bound variables and meta-variables. Its typing discipline is derived from contextual modal type theory. They first present a dependently typed lambda calculus with explicit substitutions for ordinary variables and explicit meta-substitutions for meta-variables. They 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, they describe a bidirectional type checking algorithm which uses weak head normalization and prove soundness.
- Format: PDF
- Size: 196.93 KB