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

inhabitation problemsintersection typesnormalization propertiesprincipal typingquantitative semanticstype systems

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

(38)

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

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)