Strong normalization and typability with intersection types

DOI10.1305/ndjfl/1040067315zbMath0859.03007OpenAlexW1975280443MaRDI QIDQ1924327

Silvia Ghilezan

Publication date: 14 October 1996

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1305/ndjfl/1040067315

zbMATH Keywords

intersection type assignment systemsstrongly normalizing lambda terms

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (8)

Intersection types for explicit substitutions ⋮ Behavioural inverse limit \(\lambda\)-models ⋮ Term-space semantics of typed lambda calculus ⋮ Cut-elimination in the strict intersection type assignment system is strongly normalizing ⋮ Full intersection types and topologies in lambda calculus ⋮ Intersection Types for the Resource Control Lambda Calculi ⋮ Reducibility ⋮ Compositional characterisations of \(\lambda\)-terms using intersection types

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Principal type schemes for an extended type theory
• Complete restrictions of the intersection type discipline
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• A filter lambda model and the completeness of type assignment
• Functional Characters of Solvable Terms
• Inhabitation in Intersection and Union Type Assignment Systems
• Intensional interpretations of functionals of finite type I

This page was built for publication: Strong normalization and typability with intersection types