On bounded functional interpretations

Bounded functional interpretations are variants of functional interpretations where bounds (rather than precise witnesses) are extracted from proofs. These have been particularly useful in computationally interpreting non-computational principles such as weak König’s lemma. This paper presents a family of bounded functional interpretations — in the form of a parametrized interpretation — of both intuitionistic logic and (a fragment of) intuitionistic linear logic. We show how three different instantiations of the parameters give rise to three recently developed bounded interpretations: the bounded functional interpretation, bounded modified realizability and confined modified realizability.