Non-idempotent intersection types for the lambda-calculus

DOI10.1093/JIGPAL/JZX018MaRDI QIDQ4644585zbMATH OpenOpenAlexFDO

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

(34)

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

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)