Linear Dependent Types and Relative Completeness
Linear Dependent Types and Relative Completeness
复制标题
线性相关类型和相对完整性
DOI：
10.2168/lmcs-8(4:11)2012
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Marco Gaboardi
中科院分区：
文献类型：
--
作者：
Ugo Dal Lago;Marco Gaboardi
一个系统的线性相关类型的lambda演算与充分的高阶递归，称为dlPCF，介绍和证明的声音和相对完整的。完整性在很强的意义上成立：dlPCF不仅能够精确地捕获PCF程序的功能行为（即输出如何与输入相关），而且还能够捕获它们的一些内涵属性，即用Krivine机器评估它们的复杂性。dlPCF是围绕依赖类型和线性逻辑设计的，并在索引项的底层语言上进行参数化，索引项可以进行调优，从而牺牲完整性以换取易处理性。
A system of linear dependent types for the lambda calculus with full higher-order recursion, called dlPCF, is introduced and proved sound and relatively complete. Completeness holds in a strong sense: dlPCF is not only able to precisely capture the functional behaviour of PCF programs (i.e. how the output relates to the input) but also some of their intensional properties, namely the complexity of evaluating them with Krivine's Machine. dlPCF is designed around dependent types and linear logic and is parametrized on the underlying language of index terms, which can be tuned so as to sacrifice completeness for tractability.