Strong normalization for non-structural subtyping via saturated sets

DOI10.1016/0020-0190(96)00056-7MaRDI QIDQ1351999zbMATH OpenOpenAlexFDO

Authors 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 programmingProgramming calculiLambda calculusProgramming languagesStrong normalizationSubtyping

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• Strong normalization with non-structural subtyping
• Strong normalization in type systems: A model theoretical approach
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• Short Proofs of Strong Normalization
• scientific article; zbMATH DE number 512779

Cites work

• scientific article; zbMATH DE number 4058828 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 108434 (Why is no real title available?)
• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• scientific article; zbMATH DE number 512780 (Why is no real title available?)
• scientific article; zbMATH DE number 1555189 (Why is no real title available?)
• A proof of strong normalization for \(F_ 2\), \(F_ \omega\), and beyond
• Complete restrictions of the intersection type discipline
• Efficient inference of partial types
• Godel's interpretation of intuitionism
• Intensional interpretations of functionals of finite type I
• Normal forms have partial types
• Polymorphic type inference and containment
• Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves
• Strong normalization with non-structural subtyping
• Termination of system \(F\)-bounded: A complete proof
• The lambda calculus, its syntax and semantics
• Type inference with non-structural subtyping
• Type inference with simple subtypes

Cited in

(5)

• Simple Saturated Sets for Disjunction and Second-Order Existential Quantification
• Strong normalization with non-structural subtyping
• Incompressibility of \(H\)-free edge modification problems
• Strong normalization for typed terms with surjective pairing
• Strong normalizability of the non-deterministic catch/throw calculi

Describes a project that uses

Uses Software

• Automath

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1351999)