Edit Profile (opens in new tab) Berger, Ulrich Co-Author Distance Author ID: berger.ulrich Published as: Berger, Ulrich; Berger, U. Homepage: http://www.cs.swan.ac.uk/~csulrich/ External Links: MGP · Wikidata Documents Indexed: 62 Publications since 1990, including 1 Book 13 Contributions as Editor Software Indexed: 2 Packages Co-Authors: 42 Co-Authors with 49 Joint Publications 791 Co-Co-Authors all top 5 Co-Authors 24 single-authored 14 Seisenberger, Monika 12 Schwichtenberg, Helmut 7 Tsuiki, Hideki 6 Spreen, Dieter 4 Hou, Tie 3 Berardi, Stefano 3 Setzer, Anton 3 van Bakel, Steffen 2 Blanck, Jens 2 Brattka, Vasco 2 Lawrence, Andrew 2 Miyamoto, Kenji 2 Oliva, Paulo 2 Petrovska, Olga 2 Schuster, Peter Michael 1 Abdul Rauf, Rose H. 1 Aehlig, Klaus 1 Bauer, Andrej 1 Beckmann, Arnold 1 Benl, Holger 1 Berghofer, Stefan 1 Buchholz, Wilfried 1 Diener, Hannes 1 Eberl, Matthias 1 Fouché, Willem Louw 1 Franklin, Johanna N. Y. 1 Grune, Ansgar 1 Hofmann, Martin 1 Hötzel Escardó, Martín 1 Jones, Alison 1 Keimel, Klaus 1 Køber, Petter Kristian 1 Letouzey, Pierre 1 Löwe, Benedikt 1 Manea, Florin 1 Matthes, Ralph 1 Mislove, Michael W. 1 Morozov, Andreĭ Sergeevich 1 Nordvall Forsberg, Fredrik 1 Osswald, Horst 1 Pauly, Arno M. 1 Selivanov, Viktor L’vovich 1 Tucker, John V. 1 Woods, Gregory J. M. 1 Ziegler, Martin 1 Zuber, Wolfgang all top 5 Serials 8 Annals of Pure and Applied Logic 6 Mathematical Structures in Computer Science 4 Logical Methods in Computer Science 3 Theory of Computing Systems 2 Lecture Notes in Computer Science 2 Journal of Logic and Analysis 1 Studia Logica 1 Theoretical Computer Science 1 Information and Computation 1 Journal of Automated Reasoning 1 Journal of Logic and Computation 1 Games and Economic Behavior 1 Applied Categorical Structures 1 Mathematical Logic Quarterly (MLQ) 1 Journal of Universal Computer Science 1 NATO ASI Series. Series F. Computer and Systems Sciences 1 Synthese Library 1 Electronic Notes in Theoretical Computer Science 1 Ontos Mathematical Logic 1 Journal of Logical and Algebraic Methods in Programming 1 Electronic Proceedings in Theoretical Computer Science (EPTCS) all top 5 Fields 57 Mathematical logic and foundations (03-XX) 47 Computer science (68-XX) 13 General and overarching topics; collections (00-XX) 2 Order, lattices, ordered algebraic structures (06-XX) 2 General topology (54-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 54 Publications have been cited 302 times in 170 Documents Cited by ▼ Year ▼ Total sets and objects in domain theory. Zbl 0776.03031 Berger, Ulrich 24 1993 Program extraction from normalization proofs. Zbl 0788.68015 Berger, Ulrich 17 1993 Refined program extraction from classical proofs. Zbl 0992.03070 Berger, Ulrich; Buchholz, Wilfried; Schwichtenberg, Helmut 16 2002 Modified bar recursion and classical dependent choice. Zbl 1081.03059 Berger, Ulrich; Oliva, Paulo 13 2005 Proof theory at work: Program development in the minlog system. Zbl 1015.68177 Benl, Holger; Berger, Ulrich; Schwichtenberg, Helmut; Seisenberger, Monika; Zuber, Wolfgang 13 1998 From coinductive proofs to exact real arithmetic: theory and applications. Zbl 1218.03036 Berger, Ulrich 13 2011 Modified bar recursion. Zbl 1101.03032 Berger, Ulrich; Oliva, Paulo 12 2006 Term rewriting for normalization by evaluation. Zbl 1054.68078 Berger, Ulrich; Eberl, Matthias; Schwichtenberg, Helmut 11 2003 Totale Objekte und Mengen in der Bereichstheorie. (Total objects and sets in domain theory). Zbl 0733.03037 Berger, Ulrich 11 1990 Minlog – a tool for program extraction supporting algebras and coalgebras. Zbl 1344.68201 Berger, Ulrich; Miyamoto, Kenji; Schwichtenberg, Helmut; Seisenberger, Monika 11 2011 On the stability of cooperation under indirect reciprocity with first-order information. Zbl 1394.91037 Berger, Ulrich; Grüne, Ansgar 10 2016 Uniform Heyting arithmetic. Zbl 1081.03057 Berger, Ulrich 10 2005 From coinductive proofs to exact real arithmetic. Zbl 1218.03035 Berger, Ulrich 9 2009 The Warshall algorithm and Dickson’s lemma: Two examples of realistic program extraction. Zbl 0958.03009 Berger, Ulrich; Schwichtenberg, Helmut; Seisenberger, Monika 9 2001 Proofs, programs, processes. Zbl 1280.68078 Berger, Ulrich; Seisenberger, Monika 9 2012 Logic for Gray-code computation. Zbl 1433.03120 Berger, Ulrich; Miyamoto, Kenji; Schwichtenberg, Helmut; Tsuiki, Hideki 9 2016 An arithmetic for non-size-increasing polynomial-time computation. Zbl 1064.03036 Aehlig, Klaus; Berger, Ulrich; Hofmann, Martin; Schwichtenberg, Helmut 8 2004 Reuniting the antipodes—constructive and nonstandard views of the continuum. Symposium proceedings, San Servolo, Venice, Italy, May 16–22, 1999. Zbl 0982.00037 8 2001 Intuitionistic fixed point logic. Zbl 1498.03065 Berger, Ulrich; Tsuiki, Hideki 8 2021 Realisability for induction and coinduction with applications to constructive analysis. Zbl 1219.03074 Berger, Ulrich 8 2010 Program extraction from normalization proofs. Zbl 1095.03016 Berger, Ulrich; Berghofer, Stefan; Letouzey, Pierre; Schwichtenberg, Helmut 8 2006 Coinduction for exact real number computation. Zbl 1166.68015 Berger, Ulrich; Hou, Tie 6 2008 Continuous semantics for strong normalization. Zbl 1113.68418 Berger, Ulrich 5 2005 Proofs, programs, processes. Zbl 1280.68077 Berger, Ulrich; Seisenberger, Monika 5 2010 Program extraction from classical proofs. Zbl 1540.03018 Berger, Ulrich; Schwichtenberg, Helmut 5 1995 Program development by proof transformation. Zbl 0856.03010 Berger, Ulrich; Schwichtenberg, Helmut 4 1995 Continuous functionals of dependent and transfinite types. Zbl 0946.03068 Berger, Ulrich 4 1999 Extracting imperative programs from proofs: In-place Quicksort. Zbl 1359.68042 Berger, Ulrich; Seisenberger, Monika; Woods, Gregory J. M. 4 2014 Optimized program extraction for induction and coinduction. Zbl 1509.03089 Berger, Ulrich; Petrovska, Olga 4 2018 Strong normalization for applied lambda calculi. Zbl 1125.03014 Berger, Ulrich 4 2005 Computability and totality in domains. Zbl 1005.68040 Berger, Ulrich 3 2002 A coinductive approach to computing with compact sets. Zbl 1396.03085 Berger, Ulrich; Spreen, Dieter 3 2016 Extracting non-deterministic concurrent programs. Zbl 1369.68128 Berger, Ulrich 3 2016 Extracting verified decision procedures: DPLL and resolution. Zbl 1448.68454 Berger, Ulrich; Lawrence, Andrew; Forsberg, Fredrik Nordvall; Seisenberger, Monika 2 2015 Density theorems for the domains-with-totality semantics of dependent types. Zbl 0933.03078 Berger, Ulrich 2 1999 Applications of inductive definitions and choice principles to program synthesis. Zbl 1096.03068 Berger, Ulrich; Seisenberger, Monika 2 2005 Logical approaches to computational barriers. Second conference on computability in Europe, CiE 2006, Swansea, UK, June 30–July 5, 2006. Proceedings. Zbl 1102.68002 2 2006 Prawf: an interactive proof system for program extraction. Zbl 07633503 Berger, Ulrich; Petrovska, Olga; Tsuiki, Hideki 2 2020 Program extraction from Gentzen’s proof of transfinite induction up to \(\epsilon_0\). Zbl 1024.03059 Berger, Ulrich 1 2001 Realisability and adequacy for (co)induction. Zbl 1247.03126 Berger, Ulrich 1 2009 A realizability interpretation of Church’s simple theory of types. Zbl 1423.03044 Berger, Ulrich; Hou, Tie 1 2017 Preface to the special issue: Computing with infinite data: topological and logical foundations. Zbl 1362.00034 1 2015 Typed vs. untyped realizability. Zbl 1342.68047 Berger, Ulrich; Hou, Tie 1 2012 Effectivity and density in domains: A survey. Zbl 0958.68094 Berger, Ulrich 1 1999 The greatest common divisor: a case study for program extraction from classical proofs. Zbl 1434.03024 Berger, U.; Schwichtenberg, H. 1 1996 Undecidability of equality for codata types. Zbl 1519.68145 Berger, Ulrich; Setzer, Anton 1 2018 Program extraction via typed realisability for induction and coinduction. Zbl 1244.03107 Berger, Ulrich; Seisenberger, Monika 1 2010 Programs from classical proofs. Zbl 0848.03029 Berger, Ulrich 1 1995 Minimisation vs. recursion on the partial continuous functionals. Zbl 1023.03041 Berger, Ulrich 1 2002 Extracting total Amb programs from proofs. Zbl 1528.68077 Berger, Ulrich; Tsuiki, Hideki 1 2022 A domain model characterising strong normalisation. Zbl 1153.03006 Berger, Ulrich 1 2008 Continuous semantics for strong normalisation. Zbl 1115.03008 Berger, Ulrich 1 2006 Concurrent Gaussian elimination. Zbl 1541.03182 Berger, Ulrich; Seisenberger, Monika; Spreen, Dieter; Tsuiki, Hideki 1 2023 Martin Hofmann’s case for non-strictly positive data types. Zbl 07561486 Berger, Ulrich; Matthes, Ralph; Setzer, Anton 1 2019 Concurrent Gaussian elimination. Zbl 1541.03182 Berger, Ulrich; Seisenberger, Monika; Spreen, Dieter; Tsuiki, Hideki 1 2023 Extracting total Amb programs from proofs. Zbl 1528.68077 Berger, Ulrich; Tsuiki, Hideki 1 2022 Intuitionistic fixed point logic. Zbl 1498.03065 Berger, Ulrich; Tsuiki, Hideki 8 2021 Prawf: an interactive proof system for program extraction. Zbl 07633503 Berger, Ulrich; Petrovska, Olga; Tsuiki, Hideki 2 2020 Martin Hofmann’s case for non-strictly positive data types. Zbl 07561486 Berger, Ulrich; Matthes, Ralph; Setzer, Anton 1 2019 Optimized program extraction for induction and coinduction. Zbl 1509.03089 Berger, Ulrich; Petrovska, Olga 4 2018 Undecidability of equality for codata types. Zbl 1519.68145 Berger, Ulrich; Setzer, Anton 1 2018 A realizability interpretation of Church’s simple theory of types. Zbl 1423.03044 Berger, Ulrich; Hou, Tie 1 2017 On the stability of cooperation under indirect reciprocity with first-order information. Zbl 1394.91037 Berger, Ulrich; Grüne, Ansgar 10 2016 Logic for Gray-code computation. Zbl 1433.03120 Berger, Ulrich; Miyamoto, Kenji; Schwichtenberg, Helmut; Tsuiki, Hideki 9 2016 A coinductive approach to computing with compact sets. Zbl 1396.03085 Berger, Ulrich; Spreen, Dieter 3 2016 Extracting non-deterministic concurrent programs. Zbl 1369.68128 Berger, Ulrich 3 2016 Extracting verified decision procedures: DPLL and resolution. Zbl 1448.68454 Berger, Ulrich; Lawrence, Andrew; Forsberg, Fredrik Nordvall; Seisenberger, Monika 2 2015 Preface to the special issue: Computing with infinite data: topological and logical foundations. Zbl 1362.00034 1 2015 Extracting imperative programs from proofs: In-place Quicksort. Zbl 1359.68042 Berger, Ulrich; Seisenberger, Monika; Woods, Gregory J. M. 4 2014 Proofs, programs, processes. Zbl 1280.68078 Berger, Ulrich; Seisenberger, Monika 9 2012 Typed vs. untyped realizability. Zbl 1342.68047 Berger, Ulrich; Hou, Tie 1 2012 From coinductive proofs to exact real arithmetic: theory and applications. Zbl 1218.03036 Berger, Ulrich 13 2011 Minlog – a tool for program extraction supporting algebras and coalgebras. Zbl 1344.68201 Berger, Ulrich; Miyamoto, Kenji; Schwichtenberg, Helmut; Seisenberger, Monika 11 2011 Realisability for induction and coinduction with applications to constructive analysis. Zbl 1219.03074 Berger, Ulrich 8 2010 Proofs, programs, processes. Zbl 1280.68077 Berger, Ulrich; Seisenberger, Monika 5 2010 Program extraction via typed realisability for induction and coinduction. Zbl 1244.03107 Berger, Ulrich; Seisenberger, Monika 1 2010 From coinductive proofs to exact real arithmetic. Zbl 1218.03035 Berger, Ulrich 9 2009 Realisability and adequacy for (co)induction. Zbl 1247.03126 Berger, Ulrich 1 2009 Coinduction for exact real number computation. Zbl 1166.68015 Berger, Ulrich; Hou, Tie 6 2008 A domain model characterising strong normalisation. Zbl 1153.03006 Berger, Ulrich 1 2008 Modified bar recursion. Zbl 1101.03032 Berger, Ulrich; Oliva, Paulo 12 2006 Program extraction from normalization proofs. Zbl 1095.03016 Berger, Ulrich; Berghofer, Stefan; Letouzey, Pierre; Schwichtenberg, Helmut 8 2006 Logical approaches to computational barriers. Second conference on computability in Europe, CiE 2006, Swansea, UK, June 30–July 5, 2006. Proceedings. Zbl 1102.68002 2 2006 Continuous semantics for strong normalisation. Zbl 1115.03008 Berger, Ulrich 1 2006 Modified bar recursion and classical dependent choice. Zbl 1081.03059 Berger, Ulrich; Oliva, Paulo 13 2005 Uniform Heyting arithmetic. Zbl 1081.03057 Berger, Ulrich 10 2005 Continuous semantics for strong normalization. Zbl 1113.68418 Berger, Ulrich 5 2005 Strong normalization for applied lambda calculi. Zbl 1125.03014 Berger, Ulrich 4 2005 Applications of inductive definitions and choice principles to program synthesis. Zbl 1096.03068 Berger, Ulrich; Seisenberger, Monika 2 2005 An arithmetic for non-size-increasing polynomial-time computation. Zbl 1064.03036 Aehlig, Klaus; Berger, Ulrich; Hofmann, Martin; Schwichtenberg, Helmut 8 2004 Term rewriting for normalization by evaluation. Zbl 1054.68078 Berger, Ulrich; Eberl, Matthias; Schwichtenberg, Helmut 11 2003 Refined program extraction from classical proofs. Zbl 0992.03070 Berger, Ulrich; Buchholz, Wilfried; Schwichtenberg, Helmut 16 2002 Computability and totality in domains. Zbl 1005.68040 Berger, Ulrich 3 2002 Minimisation vs. recursion on the partial continuous functionals. Zbl 1023.03041 Berger, Ulrich 1 2002 The Warshall algorithm and Dickson’s lemma: Two examples of realistic program extraction. Zbl 0958.03009 Berger, Ulrich; Schwichtenberg, Helmut; Seisenberger, Monika 9 2001 Reuniting the antipodes—constructive and nonstandard views of the continuum. Symposium proceedings, San Servolo, Venice, Italy, May 16–22, 1999. Zbl 0982.00037 8 2001 Program extraction from Gentzen’s proof of transfinite induction up to \(\epsilon_0\). Zbl 1024.03059 Berger, Ulrich 1 2001 Continuous functionals of dependent and transfinite types. Zbl 0946.03068 Berger, Ulrich 4 1999 Density theorems for the domains-with-totality semantics of dependent types. Zbl 0933.03078 Berger, Ulrich 2 1999 Effectivity and density in domains: A survey. Zbl 0958.68094 Berger, Ulrich 1 1999 Proof theory at work: Program development in the minlog system. Zbl 1015.68177 Benl, Holger; Berger, Ulrich; Schwichtenberg, Helmut; Seisenberger, Monika; Zuber, Wolfgang 13 1998 The greatest common divisor: a case study for program extraction from classical proofs. Zbl 1434.03024 Berger, U.; Schwichtenberg, H. 1 1996 Program extraction from classical proofs. Zbl 1540.03018 Berger, Ulrich; Schwichtenberg, Helmut 5 1995 Program development by proof transformation. Zbl 0856.03010 Berger, Ulrich; Schwichtenberg, Helmut 4 1995 Programs from classical proofs. Zbl 0848.03029 Berger, Ulrich 1 1995 Total sets and objects in domain theory. Zbl 0776.03031 Berger, Ulrich 24 1993 Program extraction from normalization proofs. Zbl 0788.68015 Berger, Ulrich 17 1993 Totale Objekte und Mengen in der Bereichstheorie. (Total objects and sets in domain theory). Zbl 0733.03037 Berger, Ulrich 11 1990 all cited Publications top 5 cited Publications all top 5 Cited by 168 Authors 17 Berger, Ulrich 12 Schwichtenberg, Helmut 8 Hötzel Escardó, Martín 7 Oliva, Paulo 6 Sanders, Sam 6 Spreen, Dieter 4 Aehlig, Klaus 4 Blanck, Jens 4 Hernest, Mircea-Dan 4 Normann, Dag 4 Seisenberger, Monika 4 Stoltenberg-Hansen, Viggo 4 Tsuiki, Hideki 4 Wiesnet, Franziskus 3 Avigad, Jeremy 3 Bauer, Andrej 3 Kohlenbach, Ulrich Wilhelm 3 Longley, John R. 3 Petrakis, Iosif 3 Rathjen, Michael 3 Schuster, Peter Michael 3 Trifonov, Trifon A. 2 Abel, Andreas M. 2 Allais, Guillaume 2 Aschieri, Federico 2 Bickford, Mark 2 Blot, Valentin 2 Buss, Samuel R. 2 Capretta, Venanzio 2 Dybjer, Peter 2 Eberl, Matthias 2 Haftmann, Florian 2 Hou, Tie 2 Iemhoff, Rosalie 2 Japaridze, Giorgi 2 Karádais, Basil A. 2 Katz, Mikhail G. 2 Korovina, Margarita Vladimirovna 2 Krivine, Jean-Louis 2 Kudinov, Oleg Victorovich 2 Letouzey, Pierre 2 Maietti, Maria Emilia 2 Moczydłowski, Wojciech 2 Nipkow, Tobias 2 Spitters, Bas 2 Tucker, John V. 1 Aiguier, Marc 1 Artemov, Sergei 1 Atkey, Robert 1 Bazhenov, Nikolaĭ Alekseevich 1 Benci, Vieri 1 Berghofer, Stefan 1 Biernacka, Małgorzata 1 Biernacki, Dariusz 1 Birkedal, Lars 1 Blanqui, Frédéric 1 Briseid, Eyvind Martol 1 Buchholz, Wilfried 1 Burel, Guillaume 1 Caldwell, James L. 1 Chapman, James T. E. 1 Chen, Yixiang 1 Ciobâcă, Ştefan 1 Constable, Robert Lee 1 Contente, Michele 1 Copello, Ernesto 1 Coquand, Thierry 1 Crolard, Tristan 1 Dal Lago, Ugo 1 Di Nasso, Mauro 1 Fernández, Maribel 1 Fichot, Jean 1 Fiore, Marcelo P. 1 Gaspar, Jaime 1 Gent, Ian Philip 1 Hainry, Emmanuel 1 Hameer, Aliya 1 Hayashi, Daichi 1 Hayashi, Susumu 1 Hernest, Dan 1 Hillerström, Daniel 1 Ho, Weng Kin 1 Hofmann, Martin 1 Howarth, Elizabeth 1 Ilik, Danko 1 Iordache, Viorel 1 Jaber, Guilhem 1 Jung, Achim 1 Kahle, Reinhard 1 Katz, Boris 1 Katz, Karin Usadi 1 Kavkler, Iztok 1 Kihara, Takayuki 1 Köpp, Niels 1 Köpp, Nils 1 Koprowski, Adam 1 Kraus, Nicolai 1 Krebbers, Robbert 1 Kristiansen, Lars 1 Kristiansen, Lill ...and 68 more Authors all top 5 Cited in 29 Serials 24 Theoretical Computer Science 23 Annals of Pure and Applied Logic 16 Mathematical Structures in Computer Science 12 Logical Methods in Computer Science 7 The Journal of Symbolic Logic 5 Journal of Functional Programming 3 Information and Computation 3 Theory of Computing Systems 3 The Journal of Logic and Algebraic Programming 3 Logica Universalis 2 Studia Logica 2 Journal of Automated Reasoning 2 Indagationes Mathematicae. New Series 2 Mathematical Logic Quarterly (MLQ) 2 Oberwolfach Reports 1 Computers & Mathematics with Applications 1 Siberian Mathematical Journal 1 Synthese 1 Historia Mathematica 1 Expositiones Mathematicae 1 Archive for Mathematical Logic 1 Applicable Algebra in Engineering, Communication and Computing 1 Journal of Applied Non-Classical Logics 1 The Bulletin of Symbolic Logic 1 Proceedings of the Royal Society of London. Series A. Mathematical, Physical and Engineering Sciences 1 Erkenntnis 1 Journal of Logic and Analysis 1 The Review of Symbolic Logic 1 Computability all top 5 Cited in 18 Fields 131 Mathematical logic and foundations (03-XX) 86 Computer science (68-XX) 8 Order, lattices, ordered algebraic structures (06-XX) 6 General and overarching topics; collections (00-XX) 4 Real functions (26-XX) 3 General topology (54-XX) 2 History and biography (01-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Combinatorics (05-XX) 1 Number theory (11-XX) 1 Field theory and polynomials (12-XX) 1 Commutative algebra (13-XX) 1 Algebraic geometry (14-XX) 1 Category theory; homological algebra (18-XX) 1 Measure and integration (28-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Probability theory and stochastic processes (60-XX) 1 Numerical analysis (65-XX) Citations by Year Wikidata Timeline The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.