On strong normalization and type inference in the intersection type discipline

DOI10.1016/j.tcs.2008.01.045zbMath1145.68010OpenAlexW2101641000MaRDI QIDQ930868

Gérard Boudol

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.045

zbMATH Keywords

intersection typesstrong normalizationlambda-calculustype inference

Mathematics Subject Classification ID

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

Uses Software

• Automath

Cites Work

• Principal type schemes for an extended type theory
• Principal type scheme and unification for intersection type discipline
• An extension of basic functionality theory for \(\lambda\)-calculus
• Types with intersection: An introduction
• Perpetual reductions in \(\lambda\)-calculus
• Intersection type assignment systems
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• Principality and type inference for intersection types using expansion variables
• Polar Type Inference with Intersection Types and ω
• A filter lambda model and the completeness of type assignment
• A direct proof of the finite developments theorem
• Functional Characters of Solvable Terms
• Principal Type Schemes for the Strict Type Assignment System
• Postponement, conservation and preservation of strong normalization for generalized reduction
• Types, potency, and idempotency
• Intensional interpretations of functionals of finite type I
• On the interpretation of intuitionistic number theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item