2012/02/14 by Chris Casinghino, Vilhelm Sjöberg, Stephanie Weirich
Computer Science · #cs.PL #cs.LO
paper · pdf · doi:10.4204/eptcs.76.4
published as EPTCS 76, 2012, pp. 25-39 · In Proceedings MSFP 2012, arXiv:1202.2407
arxiv created 2012/02/14 · arxiv updated 2012/02/15
The Trellys project has produced several designs for practical dependently typed languages. These languages are broken into two fragments-alogicalfragment where every term normalizes and which is consistent when interpreted as a logic, and aprogrammaticfragment 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.