Strongly Normalising Cut-Elimination with Strict Intersection Types

DOI10.1016/S1571-0661(04)80488-2zbMath1270.03034OpenAlexW2035637503MaRDI QIDQ2842832

Steffen van Bakel

Publication date: 16 August 2013

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

Full work available at URL: https://doi.org/10.1016/s1571-0661(04)80488-2

zbMATH Keywords

cut eliminationlambda calculusintersection typesterminatin

Mathematics Subject Classification ID

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

Related Items

Cut-elimination in the strict intersection type assignment system is strongly normalizing

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• 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