一般递归语言的步索引规范化
Step-Indexed Normalization for a Language with General Recursion
摘要：
Trellys项目已经为实用的依赖类型语言产生了几种设计。这些语言被分成两个片段：一个是_logical_fragment，其中每个术语都规范化，并且在解释为逻辑时是一致的，另一个是_programmatic_fragment，具有一般递归和其他方便但不可靠的特性。在本文中，我们提出了一个小的例子语言在这种风格。我们的设计允许程序员显式地提及并在两个片段之间传递信息。我们表明，这一功能大大复杂的元理论，并提出了一种新的技术，结合传统的Girard-Tait方法与步骤索引的逻辑关系，我们用它来显示规范化的逻辑片段。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
