5 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…
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…