Explicit Substitutions for Contextual Type Theory

Details Explicit Substitutions for Contextual Type Theory Explicit Substitutions for Contextual Type Theory

2010-09-14

arxiv.org/abs/1009.2789v1

EPTCS 34, 2010, pp. 5-20

Computer Science

Logic in Computer Science

In Proceedings LFMTP 2010, arXiv:1009.2189

Scientific paper

10.4204/EPTCS.34.3

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.

Affiliated with

Also associated with

No associations

Rating

Explicit Substitutions for Contextual Type Theory does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Explicit Substitutions for Contextual Type Theory, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Explicit Substitutions for Contextual Type Theory will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-76500