The Uniform Functional Interpretation with Informative Types

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. When the information takes the shape of bounds, we can recapture a form of the combination of Gödel’s functional dialectica interpretation with majorizability. When the information is “canonical” in function types, we obtain new functional interpretations and new models of Gödel’s theory T.