1 citations · 1 across the 7 of their papers we have counts for
8 papers
On the Limits of Recursive Characterizations in the Refined -Translation
Franziskus Wiesnet
This paper studies the limits of recursive classifications in proof theory and program extraction, using the refined -translation as a central example. The refined -translati…
Material Interpretation and Constructive Analysis of Maximal Ideals in
Franziskus Wiesnet
This article presents the concept of material interpretation as a method to transform classical proofs into constructive ones. Using the case study of maximal ideals in $\mathbb{Z}…
Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives
Franziskus Wiesnet
This article revisits standard theorems from elementary number theory from a constructive, algorithmic, and proof-theoretic perspective, framed within the theory of computable func…
Rates of convergence for asymptotically weakly contractive mappings in normed spaces
Thomas Powell, Franziskus Wiesnet
We study Krasnoselskii-Mann style iterative algorithms for approximating fixpoints of asymptotically weakly contractive mappings, with a focus on providing generalised convergence…
Limits of real numbers in the binary signed digit representation
Franziskus Wiesnet, Nils Köpp
We extract verified algorithms for exact real number computation from constructive proofs. To this end we use a coinductive representation of reals as streams of binary signed digi…
Logic for exact real arithmetic
Helmut Schwichtenberg, Franziskus Wiesnet
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…
An algorithmic approach to the existence of ideal objects in commutative algebra
Thomas Powell, Peter M Schuster, Franziskus Wiesnet
The existence of ideal objects, such as maximal ideals in nonzero rings, plays a crucial role in commutative algebra. These are typically justified using Zorn's lemma, and thus pos…
Limits with Signed Digit Streams
Franziskus Wiesnet
We work with the signed digit representation of abstract real numbers, which roughly is the binary representation enriched by the additional digit -1. The main objective of this pa…