18 found
Order:
See also
  1.  18
    Total Sets and Objects in Domain Theory.Ulrich Berger - 1993 - Annals of Pure and Applied Logic 60 (2):91-117.
    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.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   12 citations  
  2.  13
    Refined Program Extraction From Classical Proofs.Ulrich Berger, Wilfried Buchholz & Helmut Schwichtenberg - 2002 - Annals of Pure and Applied Logic 114 (1-3):3-25.
    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.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  3.  58
    Program Extraction From Normalization Proofs.Ulrich Berger, Stefan Berghofer, Pierre Letouzey & Helmut Schwichtenberg - 2006 - Studia Logica 82 (1):25-49.
    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.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  4.  10
    Uniform Heyting Arithmetic.Ulrich Berger - 2005 - Annals of Pure and Applied Logic 133 (1):125-148.
    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 (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  5.  13
    A Domain Model Characterising Strong Normalisation.Ulrich Berger - 2008 - Annals of Pure and Applied Logic 156 (1):39-50.
    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 (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  6.  2
    Archive for Mathematical Logic.Ulrich Berger - 2001 - Bulletin of Symbolic Logic 7 (2):280-281.
  7.  9
    Classical Truth in Higher Types.Ulrich Berger - 2008 - Mathematical Logic Quarterly 54 (3):240-246.
    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 (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  8.  9
    Foreword.Ulrich Berger, Vasco Brattka, Andrei S. Morozov & Dieter Spreen - 2012 - Annals of Pure and Applied Logic 163 (8):973-974.
  9.  34
    G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. W. Mislove and D. S. Scott, Continuous Lattices and Domains.Ulrich Berger - 2007 - Studia Logica 86 (1):137-138.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  10.  7
    Intuitionistic Fixed Point Logic.Ulrich Berger & Hideki Tsuiki - 2021 - Annals of Pure and Applied Logic 172 (3):102903.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  11.  14
    Jeremy 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]Ulrich Berger - 2002 - Bulletin of Symbolic Logic 8 (3):439-440.
  12.  4
    Review: Ulrich Kohlenbach, Mathematically Strong Subsystems of Analysis with Low Rate of Growth of Provably Recursive Functionals. [REVIEW]Ulrich Berger - 2001 - Bulletin of Symbolic Logic 7 (2):280-281.
  13.  15
    Ulrich Kohlenbach. Relative Constructivity. The Journal of Symbolic Logic, Vol. 63 , Pp. 1218–1238.Ulrich Berger - 2002 - Bulletin of Symbolic Logic 8 (3):436-437.
  14.  7
    Logic for Gray-Code Computation.Hideki Tsuiki, Helmut Schwichtenberg, Kenji Miyamoto & Ulrich Berger - 2016 - In Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science. De Gruyter. pp. 69-110.
    Direct download  
     
    Export citation  
     
    Bookmark  
  15.  14
    Review: Jeremy Avigad, A Realizability Interpretation for Classical Arithmetic. [REVIEW]Ulrich Berger - 2002 - Bulletin of Symbolic Logic 8 (3):439-440.
  16.  30
    Review: Ulrich Kohlenbach, Relative Constructivity. [REVIEW]Ulrich Berger - 2002 - Bulletin of Symbolic Logic 8 (3):436-437.
  17.  8
    Preface.Steffen van Bakel, Stefano Berardi & Ulrich Berger - 2010 - Annals of Pure and Applied Logic 161 (11):1313-1314.
  18.  4
    Preface.Steffen van Bakel, Stefano Berardi & Ulrich Berger - 2013 - Annals of Pure and Applied Logic 164 (6):589-590.