首页    期刊浏览 2024年11月25日 星期一
登录注册

文章基本信息

  • 标题:Proof nets and the call-by-value lambda-calculus
  • 本地全文:下载
  • 作者:Beniamino Accattoli
  • 期刊名称:Electronic Proceedings in Theoretical Computer Science
  • 电子版ISSN:2075-2180
  • 出版年度:2013
  • 卷号:113
  • 页码:11-26
  • DOI:10.4204/EPTCS.113.5
  • 出版社:Open Publishing Association
  • 摘要:This paper gives a detailed account of the relationship between (a variant of) the call-by-value lambda calculus and linear logic proof nets. The presentation is carefully tuned in order to realize a strong bisimulation between the two systems: every single rewriting step on the calculus maps to a single step on the nets, and viceversa. In this way, we obtain an algebraic reformulation of proof nets. Moreover, we provide a simple correctness criterion for our proof nets, which employ boxes in an unusual way.
国家哲学社会科学文献中心版权所有