lambda!-calculus, Intersection Types, and Involutions

DOI10.4230/LIPICS.FSCD.2019.15MaRDI QIDQ5089015zbMATH OpenOpenAlexFDO

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/

zbMATH Keywords

geometry of interactionintersection typesaffine combinatory algebraaffine lambda-calculus

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(1)

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

Describes a project that uses

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)