Calculating a Garbage Collector. - Ulrich Berger 001; Werner Meixner; Bernhard Möller (Methods of Programming, 1991)

An Inverse of the Evaluation Functional for Typed lambda-calculus - Ulrich Berger 001; Helmut Schwichtenberg (LICS, 1991)

Program Extraction from Normalization Proofs. - Ulrich Berger 001 (TLCA, 1993)

Total Sets and Objects in Domain Theory. - Ulrich Berger 001 (Ann. Pure Appl. Log., 1993)

Program Extraction from Classical Proofs. - Ulrich Berger 001; Helmut Schwichtenberg (LCC, 1994)

The Greatest Common Divisor: A Case Study for Program Extraction from Classical Proofs. - Ulrich Berger 001; Helmut Schwichtenberg (TYPES, 1995)

Normalisation by Evaluation. - Ulrich Berger 001; Matthias Eberl; Helmut Schwichtenberg (Prospects for Hardware Foundations, 1998)

Density Theorems for the Domains-with-Totality Semantics of Dependent Types. - Ulrich Berger 001 (Appl. Categorical Struct., 1999)

Effectivity and Density in Domains: A Survey. - Ulrich Berger 001 (Realizability Semantics and Applications@FLoC, 1999)

Program Extraction from Gentzen's Proof of Transfinite Induction up to epsilon0. - Ulrich Berger 001 (Proof Theory in Computer Science, 2001)

The Warshall Algorithm and Dickson's Lemma: Two Examples of Realistic Program Extraction. - Ulrich Berger 001; Helmut Schwichtenberg; Monika Seisenberger (J. Autom. Reason., 2001)

Preface. - Ulrich Berger 001; Karl-Heinz Niggl; Bernhard Reus (Theor. Comput. Sci., 2001)

Refined program extraction form classical proofs. - Ulrich Berger 001; Wilfried Buchholz; Helmut Schwichtenberg (Ann. Pure Appl. Log., 2002)

Computability and Totality in Domains. - Ulrich Berger 001 (Math. Struct. Comput. Sci., 2002)

Term rewriting for normalization by evaluation. - Ulrich Berger 001; Matthias Eberl; Helmut Schwichtenberg (Inf. Comput., 2003)

A Computational Interpretation of Open Induction. - Ulrich Berger 001 (LICS, 2004)

An arithmetic for non-size-increasing polynomial-time computation. - Klaus Aehlig; Ulrich Berger 001; Martin Hofmann 001; Helmut Schwichtenberg (Theor. Comput. Sci., 2004)

Applications of inductive definitions and choice principles to program synthesis. - Ulrich Berger 001; Monika Seisenberger (From sets and types to topology and analysis, 2005)

Continuous Semantics for Strong Normalization. - Ulrich Berger 001 (CiE, 2005)

An Abstract Strong Normalization Theorem. - Ulrich Berger 001 (CSL, 2005)

Continuous Semantics for Termination Proofs. - Ulrich Berger 001 (Spatial Representation, 2005)

Uniform Heyting arithmetic. - Ulrich Berger 001 (Ann. Pure Appl. Log., 2005)

Strong normalisation for applied lambda calculi - Ulrich Berger 001 (CoRR, 2005)

Strong normalization for applied lambda calculi. - Ulrich Berger 001 (Log. Methods Comput. Sci., 2005)

Functional concepts in C++. - Rose H. Abdul Rauf; Ulrich Berger 001; Anton Setzer (Trends in Functional Programming, 2006)

Continuous semantics for strong normalisation. - Ulrich Berger 001 (Math. Struct. Comput. Sci., 2006)

Modified bar recursion. - Ulrich Berger 001; Paulo Oliva (Math. Struct. Comput. Sci., 2006)

Program Extraction from Normalization Proofs. - Ulrich Berger 001; Stefan Berghofer; Pierre Letouzey; Helmut Schwichtenberg (Stud Logica, 2006)

Continuous Lattices and Domains. - Ulrich Berger 001; Gerhard Gierz; Karl Heinrich Hofmann; Klaus Keimel; Jimmie D. Lawson; Michael W. Mislove; Dana S. Scott (Stud Logica, 2007)

A domain model characterising strong normalisation. - Ulrich Berger 001 (Ann. Pure Appl. Log., 2008)

Classical truth in higher types. - Ulrich Berger 001 (Math. Log. Q., 2008)

Coinduction for Exact Real Number Computation. - Ulrich Berger 001; Tie Hou (Theory Comput. Syst., 2008)

A Provably Correct Translation of the lambda -Calculus into a Mathematical Model of C++. - Rose H. Abdul Rauf; Ulrich Berger 001; Anton Setzer (Theory Comput. Syst., 2008)

Realisability and Adequacy for (Co)induction. - Ulrich Berger 001 (CCA, 2009)

From Coinductive Proofs to Exact Real Arithmetic. - Ulrich Berger 001 (CSL, 2009)

Proofs-as-Programs in Computable Analysis. - Ulrich Berger 001 (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2009)

A coinductive approach to verified exact real number computation. - Ulrich Berger 001; Sion Lloyd (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2009)

Realisability for Induction and Coinduction with Applications to Constructive Analysis. - Ulrich Berger 001 (J. Univers. Comput. Sci., 2010)

Domain representations of spaces of compact subsets. - Ulrich Berger 001; Jens Blanck; Petter Kristian Køber (Math. Struct. Comput. Sci., 2010)

Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras. - Ulrich Berger 001; Kenji Miyamoto; Helmut Schwichtenberg; Monika Seisenberger (CALCO, 2011)

From coinductive proofs to exact real arithmetic: theory and applications - Ulrich Berger 001 (Log. Methods Comput. Sci., 2011)

Computing with Infinite Data: Topological and Logical Foundations (Dagstuhl Seminar 11411). - Ulrich Berger 001; Vasco Brattka; Victor L. Selivanov; Dieter Spreen; Hideki Tsuiki (Dagstuhl Reports, 2011)

Foreword. - Ulrich Berger 001; Vasco Brattka; Andrei S. Morozov; Dieter Spreen (Ann. Pure Appl. Log., 2012)

Typed vs. Untyped Realizability. - Ulrich Berger 001; Tie Hou (MFPS, 2012)

Preface. - Ulrich Berger 001; Michael W. Mislove (MFPS, 2012)

Extracting a DPLL Algorithm. - Andrew Lawrence; Ulrich Berger 001; Monika Seisenberger (MFPS, 2012)

Proofs, Programs, Processes. - Ulrich Berger 001; Monika Seisenberger (Theory Comput. Syst., 2012)

Extracting Imperative Programs from Proofs: In-place Quicksort. - Ulrich Berger 001; Monika Seisenberger; Gregory J. M. Woods (TYPES, 2013)

Preface. - Steffen van Bakel; Stefano Berardi; Ulrich Berger 001 (Ann. Pure Appl. Log., 2013)

Uniform Schemata for Proof Rules. - Ulrich Berger 001; Tie Hou (CiE, 2014)

Extracting verified decision procedures: DPLL and Resolution. - Ulrich Berger 001; Andrew Lawrence; Fredrik Nordvall Forsberg; Monika Seisenberger (Log. Methods Comput. Sci., 2015)

Preface. - Ulrich Berger 001; Jens Blanck; Martín Escardó; Klaus Keimel (J. Log. Algebraic Methods Program., 2015)

Preface to the special issue: Computing with infinite data: topological and logical foundations. - Ulrich Berger 001; Vasco Brattka; Victor L. Selivanov; Dieter Spreen; Hideki Tsuiki (Math. Struct. Comput. Sci., 2015)

Extracting Non-Deterministic Concurrent Programs. - Ulrich Berger 001 (CSL, 2016)

A coinductive approach to computing with compact sets. - Ulrich Berger 001; Dieter Spreen (J. Log. Anal., 2016)

Continuity, computability, constructivity: from logic to algorithms 2014 (Preface to the special issue: Continuity, Computability, Constructivity: From Logic to Algorithms 2014). - Andrej Bauer; Ulrich Berger 001; Willem L. Fouché; Dieter Spreen; Hideki Tsuiki; Martin Ziegler 001 (J. Log. Anal., 2017)

A realizability interpretation of Church's simple theory of types. - Ulrich Berger 001; Tie Hou (Math. Struct. Comput. Sci., 2017)

Optimized Program Extraction for Induction and Coinduction. - Ulrich Berger 001; Olga Petrovska (CiE, 2018)

Undecidability of Equality for Codata Types. - Ulrich Berger 001; Anton Setzer (CMCS, 2018)

Martin Hofmann's Case for Non-Strictly Positive Data Types. - Ulrich Berger 001; Ralph Matthes; Anton Setzer (TYPES, 2018)

Verification of the European Rail Traffic Management System in Real-Time Maude. - Ulrich Berger 001; Phillip James; Andrew Lawrence; Markus Roggenbach; Monika Seisenberger (Sci. Comput. Program., 2018)

Program extraction applied to monadic parsing. - Ulrich Berger 001; Alison Jones; Monika Seisenberger (J. Log. Comput., 2019)

Prawf: An Interactive Proof System for Program Extraction. - Ulrich Berger 001; Olga Petrovska; Hideki Tsuiki (CiE, 2020)

Report on BCTCS & AlgoUK 2020. - Ulrich Berger 001; Faron Moller (Bull. EATCS, 2020)

Intuitionistic fixed point logic. - Ulrich Berger 001; Hideki Tsuiki (Ann. Pure Appl. Log., 2021)

Extracting total Amb programs from proofs. - Ulrich Berger 001; Hideki Tsuiki (ESOP, 2022)

Concurrent Gaussian elimination. - Ulrich Berger 001; Monika Seisenberger; Dieter Spreen; Hideki Tsuiki (CoRR, 2023)

Computing with Infinite Objects: the Gray Code Case. - Dieter Spreen; Ulrich Berger 001 (Log. Methods Comput. Sci., 2023)

Preface of the special issue for the conference computability in Europe 2022. - Ulrich Berger 001; Johanna N. Y. Franklin; Elvira Mayordomo (Comput., 2024)