Termination of system F-bounded: A complete proof

DOI10.1006/INCO.1997.2662zbMATH Open0892.68013OpenAlexW2022460813MaRDI QIDQ1383151FDOQ1383151

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

Recommendations

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

zbMATH Keywords

system \(F\)-bounded

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• A paradigmatic object-oriented programming language: Design, static typing and semantics
• Intensional interpretations of functionals of finite type I
• Coherence of subsumption, minimum typing and type-checking in F ≤
• Simple type-theoretic foundations for object-oriented programming
• 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
• A modest model of records, inheritance, and bounded quantification
• Title not available (Why is that?)

Cited In (3)

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

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)