Program Extraction from Nested Inductive/Coinductive Definitions

Kenji Miyamoto

(LMU Munich)

We present our work on program extraction and a case study on uniformly continuous functions working in our proof system Minlog. This is a joint work with Prof. Schwichtenberg in LMU Munich.

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.
Thursday 5th July 2012, 14:00
Board Room
Department of Computer Science