License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2012.259
URN: urn:nbn:de:0030-drops-36776
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3677/
Go to the corresponding LIPIcs Volume Portal

Ehrhard, Thomas

Collapsing non-idempotent intersection types

pdf-format:
23.pdf (0.4 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{ehrhard:LIPIcs:2012:3677,
  author =	{Thomas Ehrhard},
  title =	{{Collapsing non-idempotent intersection types}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{259--273},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{Patrick C{\'e}gielski and Arnaud Durand},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3677},
  URN =		{urn:nbn:de:0030-drops-36776},
  doi =		{10.4230/LIPIcs.CSL.2012.259},
  annote =	{Keywords: Linear logic, lambda-calculus, denotational semantics}
}

Keywords: Linear logic, lambda-calculus, denotational semantics
Collection: Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL
Issue Date: 2012
Date of publication: 03.09.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI