Basic theory of \(F\)-bounded quantification.

DOI10.1006/INCO.1999.2802zbMath1045.68524OpenAlexW2000785911MaRDI QIDQ1854309

Alessandra Raffaetà, Giorgio Ghelli, Paolo Baldan

Publication date: 14 January 2003

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

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

zbMATH Keywords

binary methods

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Uses Software

• PolyTOIL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Divergence of \(F_{\leq}\) type checking
• A modest model of records, inheritance, and bounded quantification
• Bounded existentials and minimal typing
• Recursion over realizability structures
• An extension of system \(F\) with subtyping
• Decidability and confluence of \(\beta\eta\text{top}_ \leqslant\) reduction in \({\mathbb{F}}_ \leqslant\)
• Bounded quantification is undecidable
• Termination of system \(F\)-bounded: A complete proof
• Higher-order subtyping
• Unifying overloading and \(\lambda\)-abstraction: \(\lambda^{\{\,\}}\)
• Edinburgh LCF. A mechanized logic of computation
• Comparing object encodings.
• A calculus for overloaded functions with subtyping
• A proof of strong normalization for \(F_ 2\), \(F_ \omega\), and beyond
• Positive subtyping
• Integration of parametric and ``ad hoc second order polymorphism in a calculus with subtyping
• Coherence of subsumption, minimum typing and type-checking in F ≤
• Intersection types and bounded polymorphism
• A paradigmatic object-oriented programming language: Design, static typing and semantics
• A semantic basis for Quest

This page was built for publication: Basic theory of \(F\)-bounded quantification.