Logo Logo
Hilfe
Hilfe
Switch Language to English

Miyamoto, Kenji und Schwichtenberg, Helmut (2015): Program extraction in exact real arithmetic. In: Mathematical Structures in Computer Science, Bd. 25, Nr. Special issue 8: S. 1692-1704 [PDF, 159kB]

[thumbnail of program_extraction_in_exact_real_arithmetic.pdf]
Vorschau

Download (159kB)

Abstract

The importance of an abstract approach to a computation theory over general data types has been stressed by Tucker in many of his papers. Berger and Seisenberger recently elaborated the idea for extraction out of proofs involving (only) abstract reals. They considered a proof involving coinduction of the proposition that any two reals in [−1, 1] have their average in the same interval, and informally extract a Haskell program from this proof, which works with stream representations of reals. Here we formalize the proof, and machine extract its computational content using the Minlog proof assistant. This required an extension of this system to also take coinduction into account.

Dokument bearbeiten Dokument bearbeiten