lambda!-calculus, Intersection Types, and Involutions

DOI10.4230/LIPIcs.FSCD.2019.15OpenAlexW2954585109MaRDI QIDQ5089015

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

Publication date: 18 July 2022

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

zbMATH Keywords

intersection typesgeometry of interactionaffine combinatory algebraaffine lambda-calculus

Mathematics Subject Classification ID

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

Uses Software

• Erlang

Cites Work

• Unnamed Item
• Unnamed Item
• Linear realizability and full completeness for typed lambda-calculi
• A type assignment system for game semantics
• A structural approach to reversible computation
• The geometry of types
• Innocent Game Semantics via Intersection Type Assignment Systems
• A filter lambda model and the completeness of type assignment
• Games and full completeness for multiplicative linear logic
• Unique decomposition categories, Geometry of Interaction and combinatory logic
• Geometry of Interaction and linear combinatory algebras
• The involutions-as-principal types/application-as-unification Analogy
• Reversible combinatory logic
• Term Rewriting and Applications

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