Por Paolo Pistone (Università Roma Tre).
Abstract: Instantiation overflow (IO for short), first investigated by Fernando Ferreira and Gilda Ferreira, is a property of some second order types for which full comprehension for any type can be derived from comprehension restricted to atomic types. In other words, for such an A, one can type, by predicative polymorphism, “expansion terms” which realize instances of impredicative comprehension over A (i.e. the principle ∀XA ⇒A[B/X]). By this property, the usual Russell-Prawitz translation of logical connectives into System F can be "atomized", yielding derivations in System Fat.
We show that the IO property can be investigated and generalized from two related viewpoints. First, from the viewpoint of the categorial semantics of System F, the "atomization" technique corresponds to applying some permutations of rules coming from the usual dinatural interpretation of System F. As a consequence, the Russell-Prawitz translation and the "atomized" translation in Fat are observationally equivalent and, in particular, equal in the well-known class of parametric models of System F. Second, by using linear logic proof net, the IO property can be related to a geometric property of linear types. By exploiting this property we recently obtained a characterization of the simple types enjoying IO, providing a (partial) solution to a problem posed by Gilda Ferreira and Bruno Dinis.
