Intersection types for the -calculus

DOI10.23638/LMCS-14(1:2)2018MaRDI QIDQ4600774zbMATH OpenFDO

Authors Steffen Van Bakel, Franco Barbanera, Ugo de'Liguoro

Publication date 12 January 2018

Full work available at URL https://arxiv.org/abs/1704.00272

zbMATH Keywords

\(\lambda\mu\)-calculusfilter semanticsintersection typesstrong normalisation

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• A Filter Model for the λμ-Calculus
• Characterisation of strongly normalising \(\lambda\mu\)-terms
• A Translation of Intersection and Union Types for the λμ-Calculus
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
• Intersection and union types in the \(\bar{\lambda}\mu\tilde{\mu}\)-calculus

Cited in

(22)

• Intersection types and lambda models
• Compositional characterisations of \(\lambda\)-terms using intersection types
• A Translation of Intersection and Union Types for the λμ-Calculus
• Polar type inference with intersection types and
• Intersection types for light affine lambda calculus
• Intersection and union types in the \(\bar{\lambda}\mu\tilde{\mu}\)-calculus
• Strict intersection types for the lambda calculus
• Typing streams in the \({\Lambda}{\mu}\)-calculus
• Isomorphism of "Functional" Intersection Types
• Intersection types for the resource control lambda calculi
• Characterisation of normalisation properties for using strict negated intersection types
• scientific article; zbMATH DE number 1361533 (Why is no real title available?)
• Sound and complete typing for \(\lambda\mu\)
• Characterisation of strongly normalising \(\lambda\mu\)-terms
• scientific article; zbMATH DE number 7204443 (Why is no real title available?)
• Consuming and persistent types for classical logic
• Non-idempotent types for classical calculi in natural deduction style
• The approximation theorem for the \(\Lambda_{\mu}\)-calculus
• Linearization of the lambda-calculus and its relation with intersection type systems
• Types for Proofs and Programs
• Adding Negation to Lambda Mu
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage

This page was built for publication: Intersection types for the \(\lambda\mu\)-calculus

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