Program Extraction in Constructive Analysis

摘要: We sketch a development of constructive analysis in Bishop’s style, with special emphasis on low type-level witnesses (using separability the reals). The goal is to set up things such way that realistically executable programs can be extracted from proofs. This carried out for (1) Intermediate Value Theorem and (2) existence continuous inverse monotonically increasing function. Using Minlog proof assistant, proofs leading are formalized realizing terms extracted. It turns evaluating these reasonably fast algorithm compute, say, approximations √2.