Definierbare Funktionen imλ-Kalkül mit Typen. - Helmut Schwichtenberg (Arch. Math. Log., 1975)

On Bar Recursion of Types 0 and 1. - Helmut Schwichtenberg (J. Symb. Log., 1979)

Ein einfaches Verfahren zur Normalisierung unendlicher Herleitungen. - Helmut Schwichtenberg (Computation Theory and Logic, 1987)

Minimal from Classical Proofs. - Helmut Schwichtenberg (CSL, 1991)

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

An upper bound for reduction sequences in the typed λ-calculus. - Helmut Schwichtenberg (Arch. Math. Log., 1991)

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

Strict Functionals for Termination Proofs. - Jaco van de Pol; Helmut Schwichtenberg (TLCA, 1995)

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

Basic proof theory. - Anne Sjerp Troelstra; Helmut Schwichtenberg (Cambridge University Press, 1996)

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

Finite Notations for Infinite Terms. - Helmut Schwichtenberg (Ann. Pure Appl. Log., 1998)

Classifying Recursive Functions. - Helmut Schwichtenberg (Handbook of Computability Theory, 1999)

Monotone Majorizable Functionals. - Helmut Schwichtenberg (Stud Logica, 1999)

Termination of Permutative Conversions in Intuitionistic Gentzen Calculi. - Helmut Schwichtenberg (Theor. Comput. Sci., 1999)

Basic proof theory, Second Edition. - Anne Sjerp Troelstra; Helmut Schwichtenberg (Cambridge University Press, 2000)

Higher type recursion, ramification and polynomial time. - Stephen J. Bellantoni; Karl-Heinz Niggl; Helmut Schwichtenberg (Ann. Pure Appl. Log., 2000)

Linear Ramified Higher Type Recursion and Parallel Complexity. - Klaus Aehlig; Jan Johannsen; Helmut Schwichtenberg; Sebastiaan Terwijn (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)

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

A syntactical analysis of non-size-increasing polynomial time computation. - Klaus Aehlig; Helmut Schwichtenberg (ACM Trans. Comput. Log., 2002)

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

Proof Search in Minimal Logic. - Helmut Schwichtenberg (AISC, 2004)

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

A Direct Proof of the Equivalence between Brouwer's Fan Theorem and König's Lemma with a Uniqueness Hypothesis. - Helmut Schwichtenberg (J. Univers. Comput. Sci., 2005)

Inverting Monotone Continuous Functions in Constructive Analysis. - Helmut Schwichtenberg (CiE, 2006)

Minlog. - Helmut Schwichtenberg (The Seventeen Provers of the World, 2006)

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

An arithmetic for polynomial-time computation. - Helmut Schwichtenberg (Theor. Comput. Sci., 2006)

Dialectica interpretation of well-founded induction. - Helmut Schwichtenberg (Math. Log. Q., 2008)

Realizability interpretation of proofs in constructive analysis. - Helmut Schwichtenberg (Theory Comput. Syst., 2008)

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

Proofs and Computations. - Helmut Schwichtenberg; Stanley S. Wainer (Association for Symbolic Logic, 2012)

Program Extraction from Nested Definitions. - Kenji Miyamoto; Fredrik Nordvall Forsberg; Helmut Schwichtenberg (ITP, 2013)

Minimal from classical proofs. - Helmut Schwichtenberg; Christoph Senjak (Ann. Pure Appl. Log., 2013)

Program extraction in exact real arithmetic. - Kenji Miyamoto; Helmut Schwichtenberg (Math. Struct. Comput. Sci., 2015)

Editorial. - Hannes Leitgeb; Iosif Petrakis; Peter Schuster 001; Helmut Schwichtenberg (FLAP, 2016)

Embedding classical in minimal implicational logic. - Hajime Ishihara; Helmut Schwichtenberg (Math. Log. Q., 2016)

A bound for Dickson's lemma. - Josef Berger; Helmut Schwichtenberg (Log. Methods Comput. Sci., 2017)

Logic for exact real arithmetic. - Helmut Schwichtenberg; Franziskus Wiesnet (Log. Methods Comput. Sci., 2021)

Lookahead analysis in exact real arithmetic with logical methods. - Nils Köpp; Helmut Schwichtenberg (Theor. Comput. Sci., 2023)

Constructive aspects of Riemann's permutation theorem for series. - Josef Berger; Douglas S. Bridges; Hannes Diener; Helmut Schwichtenberg (Log. J. IGPL, 2025)