含一般递归语言的步索引规范化
编程语言
2012-02-15 v1 计算机科学中的逻辑
摘要
Trellys 项目已设计出多种实用的依赖类型语言方案。这些语言被划分为两个片段：一个逻辑片段，其中每个项均可规范化且在解释为逻辑时是一致的；另一个程序片段，包含一般递归及其他方便但不健全的特性。在本文中，我们提出了一种采用此风格的小型示例语言。我们的设计允许程序员显式地在两个片段之间提及并传递信息。我们表明这一特性极大地增加了元理论的复杂性，并提出了一种新技术，将传统的 Girard-Tait 方法与步索引逻辑关系相结合，用于证明逻辑片段的规范化。
引用
@article{arxiv.1202.2918,
title = {Step-Indexed Normalization for a Language with General Recursion},
author = {Chris Casinghino and Vilhelm Sjöberg and Stephanie Weirich},
journal= {arXiv preprint arXiv:1202.2918},
year = {2012}
}
备注
In Proceedings MSFP 2012, arXiv:1202.2407