Related papers: No-counterexample interpretation et sp\'{e}cificat…
We develop a correspondence between the theory of sequential algorithms and classical reasoning, via Kreisel's no-counterexample interpretation. Our framework views realizers of the no-counterexample interpretation as dynamic processes…
Almost from the inception of Hilbert's program, foundational and structural efforts in proof theory have been directed towards the goal of clarifying the computational content of modern mathematical methods. This essay surveys various…
Kohlenbach's proof mining program deals with the extraction of effective information from typically ineffective proofs. Proof mining has its roots in Kreisel's pioneering work on the so-called unwinding of proofs. The proof mining of…
Exact real computation is an alternative to floating-point arithmetic where operations on real numbers are performed exactly, without the introduction of rounding errors. When proving the correctness of an implementation, one can focus…
The aim of this paper is to highlight a hitherto unknown computational aspect of Nonstandard Analysis. Recently, a number of nonstandard versions of Goedel's system T have been introduced ([2,9,12]), and it was shown in [26] that the…
It has been shown that a functional interpretation of proofs in mathematical analysis can be given by the product of selection functions, a mode of recursion that has an intuitive reading in terms of the computation of optimal strategies in…
We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Goedel and Shoenfield can be used to rewrite proofs performed in these systems into standard ones.…
We introduce a new method, combination of random testing and abstract interpretation, for the analysis of programs featuring both probabilistic and non-probabilistic nondeterminism. After introducing "ordinary" testing, we show how to…
Ackermann's function can be expressed using an iterative algorithm, which essentially takes the form of a term rewriting system. Although the termination of this algorithm is far from obvious, its equivalence to the traditional recursive…
There are two possible computational interpretations of second-order arithmetic: Girard's system F or Spector's bar recursion and its variants. While the logic is the same, the programs obtained from these two interpretations have a…
Double-negation translations are used to encode and decode classical proofs in intuitionistic logic. We show that, in the cut-free fragment, we can simplify the translations and introduce fewer negations. To achieve this, we consider the…
We examine the convergence properties of sequences of nonnegative real numbers that satisfy a particular class of recursive inequalities, from the perspective of proof theory and computability theory. We first establish a number of results…
We describe the formalisation in Coq of a proof that the numbers e and $\pi$ are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex…
The functional interpretation is a systematic, syntactic method for transforming certain non-constructive proofs into constructive proofs with explicit bounds. We illustrate the interpretation by working through a concrete, fairly simple…
We offer a mathematical proof of consistency for Peano Arithmetic PA formalizable in PA. This result is compatible with Goedel's Second Incompleteness Theorem since our consistency proof does not rely on the representation of consistency as…
In much discussed work Artemov has recently shown that, for $\mathrm{PA}$, the consistency schema admits a form of uniform verification via selector proofs, despite the unprovability of the corresponding uniform consistency sentence…
G\"odel's second incompleteness theorem is standardly understood as showing that no sufficiently strong, consistent theory of arithmetic can prove its own consistency, a result typically interpreted against a model-theoretic background in…
We phrase parsing with context-free expressions as a type inhabitation problem where values are parse trees and types are context-free expressions. We first show how containment among context-free and regular expressions can be reduced to a…
Turing's famous 'machine' framework provides an intuitively clear conception of 'computing with real numbers'. A recursive counterexample to a theorem shows that the theorem does not hold when restricted to computable objects. These…
We present critical arguments against individual interpretation of Bohr's complementarity and Heisenberg's uncertainty principles. Statistical interpretation of these principles is discussed in the contextual framework. We support the…