Realizability interpretation of proofs in constructive analysis

We prove constructively (in the style of Bishop) that every monotone continuous function with a uniform modulus of increase has a continuous inverse. The proof is formalized, and a realizing term extracted. It turns out that even in the logical term language

• Type: Journal
• Year: 2008
• Where: MST
• Authors: Helmut Schwichtenberg
• Keywords: Continuous Inverse, Logical Term Language, MST 2008, Uniform Modulus