Explicit Substitutions for Contextual Type Theory

Download Now Free registration required

Executive Summary

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