CEMS.UL - Center for Mathematical Studies is promoting the seminar ‘The uniform functional interpretation with informative types’, with the participation of Fernando Ferreira (Faculty of Sciences of the University of Lisbon).
Abstract: We discuss a new approach to functional interpretations based on uniform quantification and relativization. The uniform quantification in the background permits a more penetrating analysis of principles related to collection and contra-collection. Relativization comes from a computationally informative notion of being an element of a given type. The approach is flexible. In the case of arithmetic, there are two natural interpretations for being an element of the ground type: the precise interpretation and the bounding interpretation. The latter is cumulative and gives rise to a form of semi-intuitionism. The interpretation of function types is not determined by the interpretation of the ground types. However, there is always a “canonical” interpretation of function types (given the interpretations of being in ground types). These canonical interpretations are new and give rise to new models of Gödel’s T. The Diller-Nahm variant of Gödel's dialectica interpretation is the non-canonical interpretation obtained by being precise at all types. A variant of the bounded functional interpretation is the non-canonical interpretation obtained by having (Bezem) bounds at all types. This latter interpretation is particularly interesting, and we also discuss it with a ground type for the real numbers.
References: F. Ferreira and P. Oliva: The uniform functional interpretation with informative types. Submitted for publication.