The heart of intersection type assignment: Normalisation proofs revisited

DOI10.1016/j.tcs.2008.01.020zbMath1145.68014OpenAlexW2074465205MaRDI QIDQ930869

Steffen van Bakel

Publication date: 24 June 2008

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

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

zbMATH Keywords

cut-eliminationapproximantsintersection typesstrong normalisation

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items

Semantic types and approximation for Featherweight Java ⋮ Intersection type assignment systems with higher-order algebraic rewriting

Cites Work

• Unnamed Item
• Cut-elimination in the strict intersection type assignment system is strongly normalizing
• Combinatory logic. With two sections by William Craig.
• Principal type schemes for an extended type theory
• The lambda calculus. Its syntax and semantics. Rev. ed.
• An extension of basic functionality theory for \(\lambda\)-calculus
• Complete restrictions of the intersection type discipline
• Intersection type assignment systems
• Normalization results for typeable rewrite systems
• A filter lambda model and the completeness of type assignment
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• Approximation and normalization results for typeable term rewriting systems
• Intensional interpretations of functionals of finite type I