Calculi with control operators have been studied as extensions of simple type theory. Real programming languages contain datatypes, so to really understand control operators, one should also include these in the calculus. As a first step in that direction, we introduce λμTλμT, a combination of Parigotʼs λμ-calculus and Gödelʼs T, to extend a calculus with control operators with a datatype of natural numbers with a primitive recursor.We consider the problem of confluence on raw terms, and that of strong normalization for (...) the well-typed terms. Observing some problems with extending the proofs of Baba et al. and Parigotʼs original confluence proof, we provide new, and improved, proofs of confluence and strong normalization for our system.We conclude with some remarks about extensions, choices, and prospects for an improved presentation. (shrink)

In view of an enhancement of our implementation on the computer, we explore the possibility of an algorithmic optimization of the various proof-theoretic techniques employed by Kohlenbach for the synthesis of new effective uniform bounds out of established qualitative proofs in Numerical Functional Analysis. Concretely, we prove that the method of “colouring” some of the quantifiers as “non-computational” extends well to ε-arithmetization, elimination-of-extensionality and model-interpretation.

We refute the conjecture that all negative translations are intuitionistically equivalent by giving two counterexamples. Then we characterise the negative translations intuitionistically equivalent to the usual ones.

This article generalises the refined A-translation method for extracting programs from classical proofs [U. Berger,W. Buchholz, H. Schwichtenberg, Refined program extraction from classical proofs, Annals of Pure and Applied Logic 114 3–25] to the scenario where additional assumptions such as choice principles are involved. In the case of choice principles, this is done by adding computational content to the ‘translated’ assumptions, an idea which goes back to [S. Berardi, M. Bezem, T. Coquand, On the computational content of the axiom of (...) choice, JSL 63 600–622] and has been further elaborated in [U. Berger, P. Oliva, Modified bar recursion and classical dependent choice, in: M. Baaz, S.D. Friedman, J. Kraijcek , Logic Colloquium ’01, in: Lecture Notes in Logic, vol. 20, Springer, Berlin, 2005, pp. 89–107]. We further investigate the applicability of this extension by means of a small but non-trivial example, and discuss the formalisation as well as some optimisations necessary in order to extract terminating programs. Both formalisation and term extraction have been implemented in the interactive proof assistant Minlog. (shrink)

We present an extension of Heyting arithmetic in finite types called Uniform Heyting Arithmetic that allows for the extraction of optimized programs from constructive and classical proofs. The system has two sorts of first-order quantifiers: ordinary quantifiers governed by the usual rules, and uniform quantifiers subject to stronger variable conditions expressing roughly that the quantified object is not computationally used in the proof. We combine a Kripke-style Friedman/Dragalin translation which is inspired by work of Coquand and Hofmann and a variant (...) of the refined A-translation due to Buchholz, Schwichtenberg and the author to extract programs from a rather large class of classical first-order proofs while keeping explicit control over the levels of recursion and the decision procedures for predicates used in the extracted program. (shrink)

From a classical proof that the gcd of natural numbers a1 and a2 is a linear combination of the two, we extract by Gödel's Dialectica interpretation an algorithm computing the coefficients. The proof uses the minimum principle. We show generally how well-founded recursion can be used to Dialectica interpret well-founded induction, which is needed in the proof of the minimum principle. In the special case of the example above it turns out that we obtain a reasonable extracted term, representing an (...) algorithm close to Euclid's. (shrink)

We upgrade the light Dialectica interpretation [6] by adding two more light universal quantifiers, which are both semi-computational and semi-uniform and complement each other. An illustrative example is presented for the new light quantifiers and a new application is given for the older uniform quantifier. The realizability of new light negative formulations for the Axiom of Choice and for the Independence of Premises is explored in the new setting.