• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Proceedings of the 2012 ACM SIGPLAN principles and practice of declarative programming >Linear Dependent Types in a Call-by-Value Scenario
【24h】

Linear Dependent Types in a Call-by-Value Scenario

机译：按值调用方案中的线性从属类型

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Linear dependent types allow to precisely capture both the extensional behavior and the time complexity of λ-terms, when the latter are evaluated by Krivine's abstract machine. In this work, we show that the same paradigm can be applied to call-by-value computation. A system of linear dependent types for Plotkin's PCF is introduced, called dℓPCF_v, whose types reflect the complexity of evaluating terms in the so-called CEK machine. DℓPCF_v is proved to be sound, but also relatively complete: every true statement about the extensional and intentional behavior of terms can be derived, provided all true index term inequalities can be used as assumptions.
机译：当由Krivine的抽象机器评估λ项时，线性相关类型允许精确地捕获其扩展行为和时间复杂度。在这项工作中，我们证明了相同的范例可以应用于按值调用计算。引入了用于Plotkin的PCF的线性相关类型的系统，称为dℓPCF_v，其类型反映了在所谓的CEK机器中评估项的复杂性。 DℓPCF_v被证明是合理的，但也相对完整：只要可以将所有真实的索引词不等式用作假设，就可以得出有关术语的扩展和故意行为的每条真实陈述。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号