Non-idempotent intersection types for the lambda-calculus

DOI10.1093/JIGPAL/JZX018MaRDI QIDQ4644585zbMATHOpenAlexFDO

Authors Antonio Bucciarelli, Delia Kesner, Daniel Lima Ventura

Publication date 8 January 2019

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/jigpal/jzx018

zbMATH Keywords

type systemsintersection typesquantitative semanticsprincipal typinginhabitation problemsnormalization properties

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Intersection types and λ-definability
• Intersection types for λGtz-calculus
• Strict intersection types for the lambda calculus
• Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
• Non-idempotent intersection types and strong normalisation

Cited in

(26)

• Intersection types for light affine lambda calculus
• Strict intersection types for the lambda calculus
• Quantitative weak linearisation
• The spirit of node replication
• scientific article; zbMATH DE number 7756108 (Why is no real title available?)
• Non finitely generated types and λ-terms combinatoric representation cost
• The bang calculus revisited
• Non-idempotent intersection types in logical form
• The Inhabitation Problem for Non-idempotent Intersection Types
• Resourceful program synthesis from graded linear types
• Linearization of the lambda-calculus and its relation with intersection type systems
• Strong call-by-value and multi types
• Tight typings and split bounds, fully developed
• Inhabitation for non-idempotent intersection types
• Structural rules and algebraic properties of intersection types
• Type inference for rank-2 intersection types using set unification
• scientific article; zbMATH DE number 7526055 (Why is no real title available?)
• The bang calculus revisited
• Quantitative global memory
• scientific article; zbMATH DE number 7559299 (Why is no real title available?)
• Compositional characterisations of \(\lambda\)-terms using intersection types
• scientific article; zbMATH DE number 7155170 (Why is no real title available?)
• Types for Proofs and Programs
• Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
• Intersection types and lambda models
• Node Replication: Theory And Practice

This page was built for publication: Non-idempotent intersection types for the lambda-calculus

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