×
Author ID: berger.ulrich Recent zbMATH articles by "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

Publications by Year

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 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

Citations by Year

The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.