System F-bounded is a second-order typed lambda calculus, where the basic features of object-oriented languages can be naturally modelled. F-bounded extends the better known system F , in a way that provides an immediate solution for the treatment of the so-called ``binary methods.'' Although more powerful than F and also quite natural, system F-bounded has only been superficially studied from a foundational perspective and many of its essential properties have been conjectured but never proved in the literature. The aim of this paper is to give a solid foundation to F-bounded, by addressing and proving the key properties of the system. In particular, transitivity elimination, completeness of the type checking semi-algorithm, the subject reduction property for ;' reduction, conser- vativity with respect to system F , and antisymmetry of a ``full'' sub- system are considered, and various possible formulations for system F-bounded are compared. Finally, a semantic interpretation of system F-bounded is presented, based on partial equivalence relations.

Basic Theory of F-bounded quantification

RAFFAETA', Alessandra
1999-01-01

Abstract

System F-bounded is a second-order typed lambda calculus, where the basic features of object-oriented languages can be naturally modelled. F-bounded extends the better known system F , in a way that provides an immediate solution for the treatment of the so-called ``binary methods.'' Although more powerful than F and also quite natural, system F-bounded has only been superficially studied from a foundational perspective and many of its essential properties have been conjectured but never proved in the literature. The aim of this paper is to give a solid foundation to F-bounded, by addressing and proving the key properties of the system. In particular, transitivity elimination, completeness of the type checking semi-algorithm, the subject reduction property for ;' reduction, conser- vativity with respect to system F , and antisymmetry of a ``full'' sub- system are considered, and various possible formulations for system F-bounded are compared. Finally, a semantic interpretation of system F-bounded is presented, based on partial equivalence relations.
1999
153
File in questo prodotto:
File Dimensione Formato  
F-Bounded.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Accesso gratuito (solo visione)
Dimensione 403.82 kB
Formato Adobe PDF
403.82 kB Adobe PDF   Visualizza/Apri

I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10278/14775
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 5
social impact