2010/09/14 by Andreas Abel, Brigitte Pientka
Computer Science · #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.34.3
published as EPTCS 34, 2010, pp. 5-20 · In Proceedings LFMTP 2010, arXiv:1009.2189
arxiv created 2010/09/14 · arxiv updated 2010/09/16
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.