lambda!-calculus, Intersection Types, and Involutions

DOI10.4230/LIPICS.FSCD.2019.15OpenAlexW2954585109MaRDI QIDQ5089015FDOQ5089015

Authors: Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, Ivan Scagnetto 

Publication date: 18 July 2022

Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2019/10522/pdf/LIPIcs-FSCD-2019-15.pdf/

Recommendations

• The involutions-as-principal types/application-as-unification analogy
• Intersection types and lambda models
• Intersection types for light affine lambda calculus
• Intersection types and computational rules
• Infinite intersection types

zbMATH Keywords

geometry of interactionintersection typesaffine combinatory algebraaffine lambda-calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx)

Cites Work

• A structural approach to reversible computation
• Geometry of Interaction and linear combinatory algebras
• A type assignment system for game semantics
• A filter lambda model and the completeness of type assignment
• Title not available (Why is that?)
• Title not available (Why is that?)
• Linear realizability and full completeness for typed lambda-calculi
• Term Rewriting and Applications
• Games and full completeness for multiplicative linear logic
• Unique decomposition categories, Geometry of Interaction and combinatory logic
• Reversible combinatory logic
• The geometry of types
• Innocent game semantics via intersection type assignment systems
• The involutions-as-principal types/application-as-unification analogy

Cited In (1)

• Term collections in {\(\lambda\)} and {\(\rho\)}-calculi

Uses Software

• Erlang

This page was built for publication: lambda!-calculus, Intersection Types, and Involutions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5089015)