Ulrich Berger and Monika Seisenberger inductively/coinductively defined a predicate of the uniform continuity and informally extracted Haskell programs from their constructive proofs of it. Our work enriches the Theory of Computable Functionals and its computer implementation Minlog in order to formalize case studies by Berger and Seisenberger.

We extract from formal proofs programs which translate a uniformly continuous function on Cauchy reals in [-1,1] into a non-well founded tree representation, and vice versa. Via Kreisel's modified realizability interpretation, the extracted programs involve certain recursion and corecursion operators which come from nested inductive/coinductive definitions. The non-well founded tree representation of uniformly continuous functions is of ground type. In this way, we manage to understand uniformly continuous functions through approximating non-well founded objects.

Board Room

Department of Computer Science