Structural rules and algebraic properties of intersection types

DOI10.1007/978-3-031-17715-6_6MaRDI QIDQ6164466zbMATH OpenOpenAlexFDO

Authors Sandra Alves, Mário Florido

Publication date 28 July 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2204.12376

zbMATH Keywords

intersection typeslinearizationsubstructural type systems

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Abstract: In this paper we define several notions of term expansion, used to define terms with less sharing, but with the same computational properties of terms typable in an intersection type system. Expansion relates terms typed by associative, commutative and idempotent intersections with terms typed in the Curry type system and the relevant type system, terms typed by non-idempotent intersections with terms typed in the affine and linear type systems and terms typed by non-idempotent and non-commutative intersections with terms typed in an ordered type system. Finally, we show how idempotent intersection is related with the contraction rule, commutative intersection with the exchange rule and associative intersection with the lack of structural rules in a type system.

Cites work

• A filter lambda model and the completeness of type assignment
• A linearization of the Lambda-calculus and consequences
• A tale of intersection types
• An Explicit Formula for the Free Exponential Modality of Linear Logic
• An extension of basic functionality theory for -calculus
• An infinitary affine lambda-calculus isomorphic to the full lambda-calculus
• Combinatory logic. With two sections by William Craig.
• Elaborating intersection and union types
• Example-directed synthesis: a type-theoretic interpretation
• From polyvariant flow information to intersection and union types
• Functional Characters of Solvable Terms
• Functionality in Combinatory Logic
• scientific article; zbMATH DE number 5852776 (Why is no real title available?)
• scientific article; zbMATH DE number 3504935 (Why is no real title available?)
• scientific article; zbMATH DE number 1330453 (Why is no real title available?)
• scientific article; zbMATH DE number 1042221 (Why is no real title available?)
• scientific article; zbMATH DE number 1956517 (Why is no real title available?)
• scientific article; zbMATH DE number 1479634 (Why is no real title available?)
• scientific article; zbMATH DE number 194911 (Why is no real title available?)
• scientific article; zbMATH DE number 1907195 (Why is no real title available?)
• Intersection types for light affine lambda calculus
• Linear logic
• Linearization of the lambda-calculus and its relation with intersection type systems
• Non-idempotent intersection types for the lambda-calculus
• Structural rules and algebraic properties of intersection types
• The Mathematics of Sentence Structure
• Types, potency, and idempotency: why nonlinearity and amnesia make a type system work
• Uniformity and the Taylor expansion of ordinary lambda-terms
• Weak linearization of the lambda calculus

Cited in

(2)

• scientific article; zbMATH DE number 1929308 (Why is no real title available?)
• Structural rules and algebraic properties of intersection types

This page was built for publication: Structural rules and algebraic properties of intersection types

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