2026-07-22T08:26:36Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3677 2024-03-06T10:34:21Z ddc:004 open_access

Collapsing non-idempotent intersection types Ehrhard, Thomas Linear logic lambda-calculus denotational semantics 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Thomas Ehrhard 2012 Is Part Of LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2012.259 urn:nbn:de:0030-drops-36776 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.259 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode