Strong normalization for non-structural subtyping via saturated sets

DOI10.1016/0020-0190(96)00056-7zbMath0875.68219OpenAlexW1970921004MaRDI QIDQ1351999

Jakob Rehof

Publication date: 27 February 1997

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0020-0190(96)00056-7

zbMATH Keywords

Functional programmingStrong normalizationLambda calculusProgramming calculiProgramming languagesSubtyping

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Related Items (1)

Incompressibility of \(H\)-free edge modification problems

Uses Software

• Automath

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
• Polymorphic type inference and containment
• The lambda calculus, its syntax and semantics
• Complete restrictions of the intersection type discipline
• Normal forms have partial types
• Efficient inference of partial types
• Type inference with non-structural subtyping
• Termination of system \(F\)-bounded: A complete proof
• A proof of strong normalization for \(F_ 2\), \(F_ \omega\), and beyond
• Godel's interpretation of intuitionism
• Strong normalization with non-structural subtyping
• Type inference with simple subtypes
• Intensional interpretations of functionals of finite type I

This page was built for publication: Strong normalization for non-structural subtyping via saturated sets