2026-07-22T00:08:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10522 2024-03-06T10:46:08Z ddc:004 open_access

lambda!-calculus, Intersection Types, and Involutions Ciaffaglione, Alberto Di Gianantonio, Pietro Honsell, Furio Lenisa, Marina Scagnetto, Ivan Affine Combinatory Algebra Affine Lambda-calculus Intersection Types Geometry of Interaction Abramsky’s affine combinatory algebras are models of affine combinatory logic, which refines standard combinatory logic in the direction of Linear Logic. Abramsky introduced various universal models of computation based on affine combinatory algebras, consisting of partial involutions over a suitable formal language {of moves}, in order to discuss reversible computation in a Geometry of Interaction setting. We investigate partial involutions from the point of view of the model theory of lambda!-calculus. The latter is a refinement of the standard lambda-calculus, corresponding to affine combinatory logic. We introduce intersection type systems for the lambda!-calculus, by extending standard intersection types with a !_u-operator. These induce affine combinatory algebras, and, via suitable quotients, models of the lambda!-calculus. In particular, we introduce an intersection type system for assigning principal types to lambda!-terms, and we state a correspondence between the partial involution interpreting a combinator and the principal type of the corresponding lambda!-term. This analogy allows for explaining as unification between principal types the somewhat awkward linear application of involutions arising from Geometry of Interaction. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alberto Ciaffaglione and Pietro Di Gianantonio and Furio Honsell and Marina Lenisa and Ivan Scagnetto 2019 Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2019.15 urn:nbn:de:0030-drops-105228 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.15 eng https://creativecommons.org/licenses/by/3.0/legalcode