Intersection types and λ-definability

DOI10.1017/S0960129502003833MaRDI QIDQ4405687zbMATH OpenOpenAlexFDO

Authors Antonio Bucciarelli, Adolfo Piperno, Ivano Salvo

Publication date 8 February 2004

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0960129502003833

zbMATH Keywords

Curry typesfunction definabilityintersection typeslambda calculustyping

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• Intersection-types à la Church
• Intersection types for combinatory logic
• Toward isomorphism of intersection and union types
• Intersection types for λGtz-calculus
• Strict intersection types for the lambda calculus

Cited in

(14)

• How to think of intersection types as Cartesian products
• Typing and computational properties of lambda expressions
• Compositional characterisations of \(\lambda\)-terms using intersection types
• A type assignment for -calculus complete both for FPTIME and strong normalization
• A Translation of Intersection and Union Types for the λμ-Calculus
• Strict intersection types for the lambda calculus
• INTERDEFINABILITY OF LAMBEKIAN FUNCTORS
• scientific article; zbMATH DE number 1759417 (Why is no real title available?)
• Non-idempotent intersection types for the lambda-calculus
• scientific article; zbMATH DE number 1361533 (Why is no real title available?)
• Intersection types and computational rules
• Toward isomorphism of intersection and union types
• The -calculus: syntax and types
• Strong normalization through idempotent intersection types: a new syntactical approach

This page was built for publication: Intersection types and λ-definability

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