一句话：在 Minlog 中形式化共归纳实数流，并从证明中提取精确实数除法算法，再转译到 Haskell 运行。
本文延续 Berger、Miyamoto、Tsuiki 等人的工作，研究如何从形式证明中提取精确实数算术算法。实数被表示为带符号数字流，其性质用余归纳定义的谓词描述，相关证明也使用余归纳。作者在证明助手 Minlog 中构造并机器检查这些证明，依托一种可处理有穷与无穷数据的类型论，将证明的计算内容抽取为项。抽取结果给出实数除法算法；随后将项翻译到 Haskell 并进行运行实验，验证了提取算法的可行性。
Continuing earlier work of the first author with U. Berger, K. Miyamoto and H. Tsuiki, it is shown how a division algorithm for real numbers given as a stream of signed digits can be extracted from an appropriate formal proof. The property of being a real number represented as a stream is formulated by means of coinductively defined predicates, and formal proofs involve coinduction. The proof assistant Minlog is used to generate the formal proofs and extract their computational content as terms of the underlying theory, a form of type theory for finite or infinite data. Some experiments with running the extracted term are described, after its translation to Haskell.