Compositional characterisations of \(\lambda\)-terms using intersection types

DOI10.1016/J.TCS.2005.03.011zbMath1077.68017OpenAlexW2006005127MaRDI QIDQ2566033

Furio Honsell, Mariangiola Dezani-Ciancaglini, Yoko Motohama

Publication date: 22 September 2005

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2005.03.011

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (8)

Intersection types and lambda models ⋮ Execution time of λ-terms via denotational semantics and intersection types ⋮ Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca ⋮ An irregular filter model ⋮ Recursive Domain Equations of Filter Models ⋮ 2008 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '08 ⋮ Types for Hereditary Head Normalizing Terms ⋮ Pre-grammars and inhabitation for a subset of rank 2 intersection types

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Type theories, normal forms, and \(D_{\infty}\)-lambda-models
• An extension of basic functionality theory for \(\lambda\)-calculus
• Domain theory in logical form
• Complete restrictions of the intersection type discipline
• An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus
• Full abstraction in the lazy lambda calculus
• Semantical analysis of perpetual strategies in \(\lambda\)-calculus
• Set-theoretical and other elementary models of the \(\lambda\)-calculus
• From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models
• Typing and computational properties of lambda expressions
• Strong normalization and typability with intersection types
• Toposes, algebraic geometry and logic. Dalhousie University, Halifax, January 16-19, 1971
• A filter lambda model and the completeness of type assignment
• A complete characterization of complete intersection-type preorders

This page was built for publication: Compositional characterisations of \(\lambda\)-terms using intersection types