Intuitionistic nonstandard bounded modified realisability and functional interpretation (Q1706266)

\textit{F. Ferreira} and \textit{P. Oliva} [Ann. Pure Appl. Logic 135, No. 1--3, 73--112 (2005; Zbl 1095.03060)] introduced bounded functional interpretation for formulae of arithmetic in all finite types with equality only for the objects of type 0 with special treatment of existential statements: it does not provide precise witnesses but only bounds for the witnesses in the sense of Howard-Bezem strong majorizability. The same idea is used in bounded realizability introduced by \textit{F. Ferreira} and \textit{A. Nunes} [J. Symb. Log. 71, No. 1, 329--346 (2006; Zbl 1100.03050)]. Intuitionistic nonstandard arithmetic $\mathsf{E}\text{-}\mathsf{HA}^\omega_{\text{st}}$ was introduced by \textit{B. van den Berg} et al. [Ann. Pure Appl. Logic 163, No. 12, 1962--1994 (2012; Zbl 1270.03121)]. It is an extension of intuitionistic arithmetic in all finite types by adding the predicate $\mathrm{st}$ and appropriate standardness axioms. The same authors defined variants of realizability and functional intepretation similar to the bounded ones, where a bound is replaced by a finite set containing a witness. In the paper under review, bounded functional interpretation and bounded realizability are transferred to $\mathsf{E}\text{-}\mathsf{HA}^\omega_{\mathrm{st}}$ formulae and are used for proving various equiconsistency, conservativity, and independence results.