Berger, U., Total sets and objects in domain theory, Annals of Pure and Applied Logic 60 91-117. Total sets and objects generalizing total functions are introduced into the theory of effective domains of Scott and Ersov. Using these notions Kreisel's Density Theorem and the Theorem of Kreisel-Lacombe-Shoenfield are generalized. As an immediate consequence we obtain the well-known continuity of computable functions on the constructive reals as well as a domain-theoretic characterization of the Heriditarily Effective Operations.

The paper presents a refined method of extracting reasonable and sometimes unexpected programs from classical proofs of formulas of the form ∀x∃yB . We also generalize previously known results, since B no longer needs to be quantifier-free, but only has to belong to a strictly larger class of so-called “goal formulas”. Furthermore we allow unproven lemmas D in the proof of ∀x∃yB , where D is a so-called “definite” formula.

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)

This paper describes formalizations of Tait's normalization proof for the simply typed λ-calculus in the proof assistants Minlog, Coq and Isabelle/HOL. From the formal proofs programs are machine-extracted that implement variants of the well-known normalization-by-evaluation algorithm. The case study is used to test and compare the program extraction machineries of the three proof assistants in a non-trivial setting.

Building on previous work by Coquand and Spiwack [T. Coquand, A. Spiwack, A proof of strong normalisation using domain theory, in: Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, LICS’06, IEEE Computer Society Press, 2006, pp. 307–316] we construct a strict domain-theoretic model for the untyped λ-calculus with pattern matching and term rewriting which has the property that a term is strongly normalising if its value is not . There are no disjointness or confluence conditions imposed (...) on the rewrite rules, and under a mild but necessary condition completeness of the method is proven. As an application, we prove strong normalisation for barrecursion in higher types combined with polymorphism and non-deterministic choice. (shrink)

We study, from a classical point of view, how the truth of a statement about higher type functionals depends on the underlying model. The models considered are the classical set-theoretic finite type hierarchy and the constructively more meaningful models of continuous functionals, hereditarily effective operations, as well as the closed term model of Gödel's system T. The main results are characterisations of prenex classes for which truth in the full set-theoretic model transfers to truth in the other models. As a (...) corollary we obtain that the axiom of choice is not conservative over Gödel's system T with classical logic for closed ∃2-formulas. We hope that this study will contribute to a clearer delineation and perception of constructive mathematics from a classical perspective. (shrink)

We study the system IFP of intuitionistic fixed point logic, an extension of intuitionistic first-order logic by strictly positive inductive and coinductive definitions. We define a realizability interpretation of IFP and use it to extract computational content from proofs about abstract structures specified by arbitrary classically true disjunction free formulas. The interpretation is shown to be sound with respect to a domain-theoretic denotational semantics and a corresponding lazy operational semantics of a functional language for extracted programs. We also show how (...) extracted programs can be translated into Haskell. As an application we extract a program converting the signed digit representation of real numbers to infinite Gray code from a proof of inclusion of the corresponding coinductive predicates. (shrink)