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

文章基本信息

  • 标题:Collapsing non-idempotent intersection types
  • 本地全文:下载
  • 作者:Thomas Ehrhard
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2012
  • 卷号:16
  • 页码:259-273
  • DOI:10.4230/LIPIcs.CSL.2012.259
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:We proved recently that the extensional collapse of the relational model of linear logic coincides with its Scott model, whose objects are preorders and morphisms are downwards closed relations. This result is obtained by the construction of a new model whose objects can be understood as preorders equipped with a realizability predicate. We present this model, which features a new duality, and explain how to use it for reducing normalization results in idempotent intersection types (usually proved by reducibility) to purely combinatorial methods. We illustrate this approach in the case of the call-by-value lambda-calculus, for which we introduce a new resource calculus, but it can be applied in the same way to many different calculi.
  • 关键词:Linear logic; lambda-calculus; denotational semantics
国家哲学社会科学文献中心版权所有