-
62Program Extraction from Normalization ProofsStudia Logica 82 (1): 25-49. 2006.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.
-
42G. gierz, K. H. Hofmann, K. keimel, J. D. Lawson, M. W. mislove and D. S. Scott, continuous lattices and domainsStudia Logica 86 (1): 137-138. 2007.
-
35Review: Ulrich Kohlenbach, Relative Constructivity (review)Bulletin of Symbolic Logic 8 (3): 436-437. 2002.
-
29Intuitionistic fixed point logicAnnals of Pure and Applied Logic 172 (3): 102903. 2021.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 operationa…Read more
-
23Total sets and objects in domain theoryAnnals of Pure and Applied Logic 60 (2): 91-117. 1993.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 He…Read more
-
21Uniform heyting arithmeticAnnals of Pure and Applied Logic 133 (1): 125-148. 2005.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 …Read more
-
21Jeremy Avigad. A realizability interpretation for classical arithmetic. Logic Colloquium '98, Proceedings of the annual European summer meeting of the Association for Symbolic Logic, held in Prague, Czech Republic, August 9–15, 1998, edited by Samuel R. Buss, Petr Hájek, and Pavel Pudák, Lecture notes in logic, no. 13, Association for Symbolic Logic, Urbana, and A K Peters, Natick, Mass., 2000, pp. 57–90 (review)Bulletin of Symbolic Logic 8 (3): 439-440. 2002.
-
20Ulrich Kohlenbach. Relative constructivity. The journal of symbolic logic, vol. 63 , pp. 1218–1238Bulletin of Symbolic Logic 8 (3): 436-437. 2002.
-
19Refined program extraction from classical proofsAnnals of Pure and Applied Logic 114 (1-3): 3-25. 2002.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
-
16Logic for Gray-code ComputationIn Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science, De Gruyter. pp. 69-110. 2016.
-
15Review: Jeremy Avigad, A Realizability Interpretation for Classical Arithmetic (review)Bulletin of Symbolic Logic 8 (3): 439-440. 2002.
-
14A domain model characterising strong normalisationAnnals of Pure and Applied Logic 156 (1): 39-50. 2008.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 co…Read more
-
11Review: Ulrich Kohlenbach, Mathematically Strong Subsystems of Analysis with Low Rate of Growth of Provably Recursive Functionals (review)Bulletin of Symbolic Logic 7 (2): 280-281. 2001.
-
11Classical truth in higher typesMathematical Logic Quarterly 54 (3): 240-246. 2008.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 t…Read more
-
5Logic, Construction, Computation (edited book)De Gruyter. 2012.Over the last few decades the interest of logicians and mathematicians in constructive and computational aspects of their subjects has been steadily growing, and researchers from disparate areas realized that they can benefit enormously from the mutual exchange of techniques concerned with those aspects. A key figure in this exciting development is the logician and mathematician Helmut Schwichtenberg to whom this volume is dedicated on the occasion of his 70th birthday and his turning emeritus. …Read more
-
3PrefaceIn Ulrich Berger, Hannes Diener, Peter Schuster & Monika Seisenberger (eds.), Logic, Construction, Computation, De Gruyter. pp. 2-4. 2012.
-
1A Realizability Interpretation For Classical Arithmetic (review)Bulletin of Symbolic Logic 8 (3): 439-439. 2002.
-
1Program Extraction via Typed Realisability for Induction and CoinductionIn Ralf Schindler (ed.), Ways of Proof Theory, De Gruyter. pp. 157-182. 2010.
-
1REVIEWS-Refined program extraction from classical proofsBulletin of Symbolic Logic 9 (1): 47-48. 2003.
-
On the Constructive and Computational Content of Abstract MathematicsIn Stefania Centrone, Sara Negri, Deniz Sarikaya & Peter M. Schuster (eds.), Mathesis Universalis, Computability and Proof, Springer Verlag. 2019.
Areas of Specialization
Science, Logic, and Mathematics |
Areas of Interest
Science, Logic, and Mathematics |