Typing untyped \(\lambda\)-terms, or reducibility strikes again!

DOI10.1016/S0168-0072(97)00047-XzbMath0930.03011OpenAlexW1520157111MaRDI QIDQ1295368

Jean H. Gallier

Publication date: 15 February 2000

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0168-0072(97)00047-x

zbMATH Keywords

reducibilitylambda calculustype assignmentnormalizable termsconjunctive typesmeta-theorems relating properties of \(\lambda\)-terms and their typabilityrealizability methodweak head-normal forms

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

Intersection types for explicit substitutions ⋮ Behavioural inverse limit \(\lambda\)-models ⋮ Intersection Types for the Resource Control Lambda Calculi ⋮ Reducibility ⋮ Normalization without reducibility

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves
• An extension of basic functionality theory for \(\lambda\)-calculus
• A proof of strong normalization for \(F_ 2\), \(F_ \omega\), and beyond
• A new type assignment for λ-terms
• Church-Rosser theorem for typed functional systems
• Functional Characters of Solvable Terms
• Intensional interpretations of functionals of finite type I