Explicit Substitutions for Contextual Type Theory

TL;DR

This paper introduces an explicit substitution calculus for contextual type theory, enabling lazy, single-pass substitution for both variables and meta-variables, with a sound bidirectional type checking algorithm.

Contribution

It presents a dependently typed lambda calculus with explicit substitutions for variables and meta-variables, along with a normalization procedure and a sound type checking algorithm.

Findings

Lazy, single-pass normalization for both variable types

Soundness of the bidirectional type checking algorithm

Explicit substitution calculus derived from modal type theory

Abstract

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.