-
1Program Extraction via Typed Realisability for Induction and CoinductionIn Ralf Schindler (ed.), Ways of Proof Theory, De Gruyter. pp. 157-182. 2010.
-
3PrefaceIn Ulrich Berger, Hannes Diener, Peter Schuster & Monika Seisenberger (eds.), Logic, Construction, Computation, De Gruyter. pp. 2-4. 2012.
-
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
-
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.
-
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.
-
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
-
15Review: Jeremy Avigad, A Realizability Interpretation for Classical Arithmetic (review)Bulletin of Symbolic Logic 8 (3): 439-440. 2002.
-
35Review: Ulrich Kohlenbach, Relative Constructivity (review)Bulletin of Symbolic Logic 8 (3): 436-437. 2002.
-
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
-
20Ulrich Kohlenbach. Relative constructivity. The journal of symbolic logic, vol. 63 , pp. 1218–1238Bulletin of Symbolic Logic 8 (3): 436-437. 2002.
-
1REVIEWS-Refined program extraction from classical proofsBulletin of Symbolic Logic 9 (1): 47-48. 2003.
-
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.
-
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.
-
1A Realizability Interpretation For Classical Arithmetic (review)Bulletin of Symbolic Logic 8 (3): 439-439. 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
-
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
-
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.
-
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.
-
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
Areas of Specialization
Science, Logic, and Mathematics |
Areas of Interest
Science, Logic, and Mathematics |