Principal types as partial involutions

DOI10.1017/S0960129524000380MaRDI QIDQ6993437zbMATH OpenFDO

Authors Furio Honsell, Marina Lenisa, Ivan Scagnetto

Publication date 25 April 2025

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0960129524000380

zbMATH Keywords

combinatory algebrasgeometry of interactionlinear affine \(\lambda\)-calculuspartial involutionsprincipal types

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A structural approach to reversible computation
• An Efficient Unification Algorithm
• BCK-combinators and linear \(\lambda\)-terms have types
• Elementary complexity and geometry of interaction
• FUNCTIONAL PEARL Linear lambda calculus and PTIME-completeness
• Games and full completeness for multiplicative linear logic
• Geometry of Interaction and linear combinatory algebras
• scientific article; zbMATH DE number 4179372 (Why is no real title available?)
• scientific article; zbMATH DE number 3889502 (Why is no real title available?)
• scientific article; zbMATH DE number 4123722 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• scientific article; zbMATH DE number 1841836 (Why is no real title available?)
• scientific article; zbMATH DE number 786500 (Why is no real title available?)
• lambda!-calculus, Intersection Types, and Involutions
• Light linear logic
• Linear realizability and full completeness for typed lambda-calculi
• New foundations for the geometry of interaction
• Principal types as nets
• Principal types of BCK-lambda-terms
• Retracing some paths in process algebra
• The involutions-as-principal types/application-as-unification analogy
• The lambda calculus. Its syntax and semantics. Rev. ed.

This page was built for publication: Principal types as partial involutions

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