Unifying functional interpretations
The author shows how different functional interpretations can be integrated in one formal framework with two parameters: The ``bounded quantifications \(\forall\;{\mathbf x} \sqsubset {\mathbf t} A({\mathbf x})\) and \(\exists\;{\mathbf x} \prec {\mathbf t} A({\mathbf x})\). The different instantiations are summarized in Table 3 (p.~287) as follows (using the author's notations): \[ \begin{alignedat}{3} &\forall\;{\mathbf x} \sqsubset {\mathbf t} w &\quad &\exists\;{\mathbf x} \prec {\mathbf t} A({\mathbf x}) &\quad &\mathbf{Functional interpretations} \\ \\ &A({\mathbf t})& &A({\mathbf t})& &\text{Dialectica interpretation (1958)} \\ &\forall\;{\mathbf x} A({\mathbf x})& &A({\mathbf t})& &\text{Modified realizability (1962)} \\ &\forall\;{\mathbf x} \in {\mathbf t} A({\mathbf x})& &A({\mathbf t})& &\text{Diller-Nahm interpretationi (1962)} \\ &\forall\;\underline{{\mathbf x}} \in \text{rng}({\mathbf t}) \forall\;\overline{{\mathbf x}} A({\mathbf x})& &A({\mathbf t})& &\text{Stein's family of interpretations (1979)} \\ &A({\mathbf t})& &\exists\;{\mathbf x} \leq^* {\mathbf t} A({\mathbf x})& &\text{Monotone Dialectica interpretation (1996)} \\ &\forall\;{\mathbf x} A({\mathbf x})& &\exists\;{\mathbf x} \leq^* {\mathbf t} A({\mathbf x})& &\text{Monotone modified realizability (1998)} \\ &\tilde{\forall} \leq^* {\mathbf t} A({\mathbf x})& &A({\mathbf t})& &\text{Bounded functional interpretation (2005).} \end{alignedat} \]
- A unified functional look at completion in MET, UNIF and AP
- Functional un\(|\)unparsing
- A parametrised functional interpretation of Heyting arithmetic
- Light Dialectica program extraction from a classical Fibonacci proof
- A new computation of the \(\Sigma\)-ordinal of \(\mathrm{KP}{\omega}\)
- Computational interpretations of classical reasoning: from the epsilon calculus to stateful programs
- scientific article; zbMATH DE number 1285772 (Why is no real title available?)
- On bounded functional interpretations
- Modal functional (``Dialectica) interpretation
- Unifying functional interpretations: past and future
- Hardwiring truth in functional interpretations
- Light Dialectica revisited
- A Gentzen-style monadic translation of Gödel's system T
- Uniform functional interpretations
- Functional interpretations of linear and intuitionistic logic
This page was built for publication: Unifying functional interpretations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q867407)
