Step-Indexed Normalization for a Language with General Recursion

Chris Casinghino
(University of Pennsylvania)
Vilhelm Sjöberg
(University of Pennsylvania)
Stephanie Weirich
(University of Pennsylvania)

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.

In James Chapman and Paul Blain Levy: Proceedings Fourth Workshop on Mathematically Structured Functional Programming (MSFP 2012), Tallinn, Estonia, 25 March 2012, Electronic Proceedings in Theoretical Computer Science 76, pp. 25–39.
Published: 11th February 2012.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: