通过指称语义和交集类型计算lambda项的执行时间
计算机科学中的逻辑
2009-05-27 v1 计算复杂性
摘要
线性逻辑的基于多重集的关联模型诱导了无类型lambda演算的一种语义，它对应于一个非幂等的交集类型系统，即系统R。我们证明，在系统R中，类型推导的大小和类型的大小与lambda项在特定环境机器（Krivine机器）中的执行时间密切相关。
引用
@article{arxiv.0905.4251,
title = {Execution Time of lambda-Terms via Denotational Semantics and Intersection Types},
author = {Daniel de Carvalho},
journal= {arXiv preprint arXiv:0905.4251},
year = {2009}
}
备注
36 pages