Termination of system F-bounded: A complete proof

DOI10.1006/INCO.1997.2662MaRDI QIDQ1383151zbMATHOpenAlexFDO

Authors G. 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)

Recommendations

• Basic theory of \(F\)-bounded quantification.
• scientific article; zbMATH DE number 814799
• scientific article; zbMATH DE number 4134006
• A proof of strong normalization for \(F_ 2\), \(F_ \omega\), and beyond

Cites work

• scientific article; zbMATH DE number 1142318 (Why is no real title available?)
• scientific article; zbMATH DE number 1479647 (Why is no real title available?)
• A modest model of records, inheritance, and bounded quantification
• A paradigmatic object-oriented programming language: Design, static typing and semantics
• A proof of strong normalization for \(F_ 2\), \(F_ \omega\), and beyond
• An extension of system \(F\) with subtyping
• Coherence of subsumption, minimum typing and type-checking in F ≤
• Decidability and confluence of \(\beta\eta\text{top}_ \leqslant\) reduction in \({\mathbb{F}}_ \leqslant\)
• Intensional interpretations of functionals of finite type I
• Simple type-theoretic foundations for object-oriented programming

Cited in

(3)

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

Describes a project that uses

Uses Software

• Automath
• PolyTOIL

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

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