Termination of system \(F\)-bounded: A complete proof

DOI10.1006/INCO.1997.2662zbMath0892.68013OpenAlexW2022460813MaRDI QIDQ1383151

Giorgio Ghelli

Publication date: 27 July 1998

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.1997.2662

zbMATH Keywords

system \(F\)-bounded

Mathematics Subject Classification ID

Theory of programming languages (68N15) Combinatory logic and lambda calculus (03B40)

Related Items (3)

Strong normalization for non-structural subtyping via saturated sets ⋮ Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions ⋮ Basic theory of \(F\)-bounded quantification.

Uses Software

• Automath
• PolyTOIL

Cites Work

• Unnamed Item
• Unnamed Item
• A modest model of records, inheritance, and bounded quantification
• An extension of system \(F\) with subtyping
• Decidability and confluence of \(\beta\eta\text{top}_ \leqslant\) reduction in \({\mathbb{F}}_ \leqslant\)
• A proof of strong normalization for \(F_ 2\), \(F_ \omega\), and beyond
• Coherence of subsumption, minimum typing and type-checking in F ≤
• A paradigmatic object-oriented programming language: Design, static typing and semantics
• Simple type-theoretic foundations for object-oriented programming
• Intensional interpretations of functionals of finite type I

This page was built for publication: Termination of system \(F\)-bounded: A complete proof