Date Added: Dec 2011
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, the authors present a small example language in this style. Their design allows the programmer to explicitly mention and pass information between the two fragments. They show that this feature substantially complicates the meta-theory and present a new technique, combining the traditional Girard-Tait method with step-indexed logical relations, which they use to show normalization for the logical fragment.