平等、准隐式乘积和大规模消除
摘要：带有等式反射的类型理论：可证等式可用于强制转换术语的类型。在术语的约简过程中，转换和其他注释，包括隐含参数，被丢弃。我们开发了一个具有未注释术语的系统的元理论，该系统是不可判定的。然后，我们设计了一个具有注释术语的可判定系统，并以未注释系统为基础进行了证明。最后，我们展示了如何通过使用我们所谓的准隐性乘积来扩展该方法来解释大规模消除。
作者：Vilhelm Sj"oberg (University of Pennsylvania), Aaron Stump (The University of Iowa)
论文ID：1101.4430
分类：Programming Languages
分类简称：cs.PL
提交时间：2011-01-25