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

文章基本信息

  • 标题:Full Abstraction for Resource Calculus with Tests
  • 本地全文:下载
  • 作者:Antonio Bucciarelli ; Alberto Carraro ; Thomas Ehrhard
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2011
  • 卷号:12
  • 页码:97-111
  • DOI:10.4230/LIPIcs.CSL.2011.97
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:We study the semantics of a resource sensitive extension of the lambda-calculus in a canonical reflexive object of a category of sets and relations, a relational version of the original Scott D infinity model of the pure lambda-calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda-calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a ``must'' parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary lambda-calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula.
  • 关键词:resource lambda calculus; relational semantics; full abstraction; differential linear logic
国家哲学社会科学文献中心版权所有