\input zb-basic
\input zb-ioport
\iteman{io-port 06244441}
\itemau{Hernest, Mircea-Dan}
\itemti{Synthesis of moduli of uniform continuity by the monotone Dialectica interpretation in the proof-system {\tt MinLog}.}
\itemso{Momigliano, Alberto (ed.) et al., Proceedings of the first international workshop on logical frameworks and meta-languages: theory and practice (LFMTP 2006), Seattle, WA, USA, August 16, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 174, No. 5, 141-149 (2007).}
\itemab
Summary: We extract on the computer a number of moduli of uniform continuity for the first few elements of a sequence of closed terms $t$ of G\"odel's $\bold T$ of type $\left(\mathbb{N}\to\mathbb{N}\right)\to\left(\mathbb{N}\to\mathbb{N}\right)$. The generic solution may then be quickly inferred by the human. The automated synthesis of such moduli proceeds from a proof of the hereditarily extensional equality ($\approx$) of $t$ to itself, hence a proof in a weakly extensional variant of Berger-Buchholz-Schwichtenberg's system $Z$ of $t\approx_{\left(\mathbb{N}\to\mathbb{N}\right)\to\left(\mathbb{N}\to\mathbb{N}\right)}t$. We use an implementation on the machine, in Schwichtenberg's {\tt MinLog} proof-system, of a non-literal adaptation to natural deduction of Kohlenbach's monotone functional interpretation. This new version of the monotone Dialectica produces terms in {\tt NbE}-normal form by means of a recurrent partial {\tt NbE}-normalization. Such partial evaluation is strictly necessary.
\itemrv{~}
\itemcc{}
\itemut{program extraction from classical proofs; complexity of extracted programs; proof- and program-extraction system {\tt MinLog}; G\"odel's functional interpretation; partial evaluation; proof mining; monotone Dialectica interpretation}
\itemli{http://www.sciencedirect.com/science/article/pii/S157106610700237X?np=y}
\end