Non-idempotent intersection types for the lambda-calculus

DOI10.1093/JIGPAL/JZX018zbMATH Open1405.03036OpenAlexW2760585651MaRDI QIDQ4644585FDOQ4644585

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

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

zbMATH Keywords

type systemsintersection typesquantitative semanticsprincipal typinginhabitation problemsnormalization properties

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cited In (27)

• Title not available (Why is that?)
• Tight typings and split bounds, fully developed
• Inhabitation for non-idempotent intersection types
• Title not available (Why is that?)
• Resourceful program synthesis from graded linear types
• Compositional characterisations of \(\lambda\)-terms using intersection types
• The spirit of node replication
• Quantitative weak linearisation
• Strong call-by-value and multi types
• Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
• Node Replication: Theory And Practice
• Strict intersection types for the lambda calculus
• Non finitely generated types and λ-terms combinatoric representation cost
• The bang calculus revisited
• Types for Proofs and Programs
• Quantitative global memory
• Intersection types for light affine lambda calculus
• The bang calculus revisited
• Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)
• Type inference for rank-2 intersection types using set unification
• Title not available (Why is that?)
• Intersection types and lambda models
• The Inhabitation Problem for Non-idempotent Intersection Types
• A strong call-by-need calculus
• Title not available (Why is that?)
• Linearization of the lambda-calculus and its relation with intersection type systems
• Structural rules and algebraic properties of intersection types

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)