Step-Indexed Normalization for a Language with General Recursion

TL;DR

This paper introduces a step-indexed normalization technique for a dependently typed language with general recursion, enabling explicit interaction between logical and programmatic fragments while ensuring normalization in the logical part.

Contribution

It presents a novel combination of Girard-Tait method with step-indexed logical relations to prove normalization in a language with both recursive and logical components.

Findings

Normalization proof for the logical fragment achieved

Explicit fragment interaction complicates metatheory

New technique combines Girard-Tait with step-indexed relations

Abstract

The Trellys project has produced several designs for practical dependently typed languages. These languages are broken into two fragments-a_logical_fragment where every term normalizes and which is consistent when interpreted as a logic, and a_programmatic_fragment with general recursion and other convenient but unsound features. In this paper, we present a small example language in this style. Our design allows the programmer to explicitly mention and pass information between the two fragments. We show that this feature substantially complicates the metatheory and present a new technique, combining the traditional Girard-Tait method with step-indexed logical relations, which we use to show normalization for the logical fragment.