> Details

Ciaffaglione, Alberto [Author]; Di Gianantonio, Pietro [Author]; Honsell, Furio [Author]; Lenisa, Marina [Author]; Scagnetto, Ivan [Author] ; Alberto Ciaffaglione and Pietro Di Gianantonio and Furio Honsell and Marina Lenisa and Ivan Scagnetto [Contributor]

lambda!-calculus, Intersection Types, and Involutions

Reference
management

Bookmarks

Remove from
bookmarks

Share this on Whatsapp

Close

Bookmarks



You can manage bookmarks using lists, please log in to your user account for this.
  • Media type: E-Article; Electronic Conference Proceeding; Text
  • Title: lambda!-calculus, Intersection Types, and Involutions
  • Contributor: Ciaffaglione, Alberto [Author]; Di Gianantonio, Pietro [Author]; Honsell, Furio [Author]; Lenisa, Marina [Author]; Scagnetto, Ivan [Author]
  • imprint: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019
  • Language: English
  • DOI: https://doi.org/10.4230/LIPIcs.FSCD.2019.15
  • Keywords: Affine Lambda-calculus ; Affine Combinatory Algebra ; Intersection Types ; Geometry of Interaction
  • Origination:
  • Footnote: Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
  • Description: 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.
  • Access State: Open Access