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-less than or equal to, in a way that provides an immediate solution for the treatment of the so-called "binary methods." Although more powerful than F-less than or equal to 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 beta eta reduction, conservativity with respect to system F-less than or equal to, and antisymmetry of a "full" subsystem 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
GHELLI, GIORGIO;
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-less than or equal to, in a way that provides an immediate solution for the treatment of the so-called "binary methods." Although more powerful than F-less than or equal to 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 beta eta reduction, conservativity with respect to system F-less than or equal to, and antisymmetry of a "full" subsystem 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
