Ciaffaglione, Alberto ;
Di Gianantonio, Pietro ;
Honsell, Furio ;
Lenisa, Marina ;
Scagnetto, Ivan
lambda!calculus, Intersection Types, and Involutions
Abstract
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 lambdacalculus, corresponding to affine combinatory logic. We introduce intersection type systems for the lambda!calculus, by extending standard intersection types with a !_uoperator. 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.
BibTeX  Entry
@InProceedings{ciaffaglione_et_al:LIPIcs:2019:10522,
author = {Alberto Ciaffaglione and Pietro Di Gianantonio and Furio Honsell and Marina Lenisa and Ivan Scagnetto},
title = {{lambda!calculus, Intersection Types, and Involutions}},
booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
pages = {15:115:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771078},
ISSN = {18688969},
year = {2019},
volume = {131},
editor = {Herman Geuvers},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/10522},
URN = {urn:nbn:de:0030drops105228},
doi = {10.4230/LIPIcs.FSCD.2019.15},
annote = {Keywords: Affine Combinatory Algebra, Affine Lambdacalculus, Intersection Types, Geometry of Interaction}
}
18.06.2019
Keywords: 

Affine Combinatory Algebra, Affine Lambdacalculus, Intersection Types, Geometry of Interaction 
Seminar: 

4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Issue date: 

2019 
Date of publication: 

18.06.2019 