Program extraction in exact real arithmetic

Miyamoto, Kenji; Schwichtenberg, Helmut (2015): Program extraction in exact real arithmetic. In: Mathematical Structures in Computer Science, Vol. 25, No. Special issue 8: pp. 1692-1704

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.

• Item Type: Journal article
• Faculties: Mathematics, Computer Science and Statistics > Mathematics
• Subjects: 500 Science > 510 Mathematics
• Alliance/National Licence: This publication is with permission of the rights owner freely accessible due to an Alliance licence and a national licence (funded by the DFG, German Research Foundation) respectively.
• Language: German