| Publication | Date of Publication | Type |
|---|
Program extraction from classical proofs
Lecture Notes in Computer Science | 2023-12-12 | Paper |
Computational Aspects of Bishop’s Constructive Mathematics
Handbook of Constructive Mathematics | 2023-08-11 | Paper |
Logic for Exact Real Arithmetic: Multiplication
Mathematics for Computation (M4C) | 2023-08-04 | Paper |
Lookahead analysis in exact real arithmetic with logical methods
Theoretical Computer Science | 2023-01-05 | Paper |
Mathematische Logik
The Legacy of Kurt Schütte | 2021-12-03 | Paper |
scientific article; zbMATH DE number 7350773 (Why is no real title available?)
(available as arXiv preprint) | 2021-05-25 | Paper |
| scientific article; zbMATH DE number 7350773 (Why is no real title available?) | 2021-05-25 | Paper |
Program extraction from proofs: the fan theorem for uniformly coconvex bars
Mathesis Universalis, Computability and Proof | 2020-08-10 | Paper |
Higman's lemma and its computational content
Advances in Proof Theory | 2020-08-07 | Paper |
Logic for Gray-code computation
Concepts of Proof in Mathematics, Philosophy, and Computer Science | 2020-04-03 | Paper |
Tiered arithmetics
Outstanding Contributions to Logic | 2020-02-05 | Paper |
Logic for exact real arithmetic
(available as arXiv preprint) | 2019-04-29 | Paper |
The greatest common divisor: A case study for program extraction from classical proofs
Lecture Notes in Computer Science | 2019-01-15 | Paper |
A bound for Dickson's lemma
(available as arXiv preprint) | 2017-10-12 | Paper |
A syntactical analysis of non-size-increasing polynomial time computation
ACM Transactions on Computational Logic | 2017-06-13 | Paper |
Program extraction in exact real arithmetic
Mathematical Structures in Computer Science | 2016-07-27 | Paper |
Embedding classical in minimal implicational logic
Mathematical Logic Quarterly (MLQ) | 2016-03-17 | Paper |
Viewing \({\lambda}\)-terms through maps
Indagationes Mathematicae. New Series | 2014-09-03 | Paper |
Program extraction from nested definitions
Interactive Theorem Proving | 2013-08-07 | Paper |
Minimal from classical proofs
Annals of Pure and Applied Logic | 2013-04-15 | Paper |
| Constructive aspects of Riemann's permutation theorem for series | 2013-03-28 | Paper |
| Proofs and computations | 2012-01-27 | Paper |
Minlog -- a tool for program extraction supporting algebras and coalgebras
Algebra and Coalgebra in Computer Science | 2011-09-02 | Paper |
| Decorating proofs | 2011-05-31 | Paper |
| Towards a formal theory of computability | 2011-03-09 | Paper |
Realizability interpretation of proofs in constructive analysis
Theory of Computing Systems | 2009-05-08 | Paper |
Program Extraction in Constructive Analysis
Synthese Library | 2009-03-12 | Paper |
Dialectica interpretation of well-founded induction
MLQ | 2008-06-12 | Paper |
| scientific article; zbMATH DE number 5269066 (Why is no real title available?) | 2008-04-29 | Paper |
| Recursion on the partial continuous functionals | 2008-04-14 | Paper |
| Constructive analysis with witnesses | 2008-01-14 | Paper |
| A direct proof of the equivalence between Brouwer's fan theorem and König's lemma with a uniqueness hypothesis | 2007-10-15 | Paper |
Logical Approaches to Computational Barriers
Lecture Notes in Computer Science | 2007-04-30 | Paper |
An arithmetic for polynomial-time computation
Theoretical Computer Science | 2006-08-16 | Paper |
Program extraction from normalization proofs
Studia Logica | 2006-03-17 | Paper |
Artificial Intelligence and Symbolic Computation
Lecture Notes in Computer Science | 2005-08-19 | Paper |
| scientific article; zbMATH DE number 2185672 (Why is no real title available?) | 2005-07-04 | Paper |
| scientific article; zbMATH DE number 2152236 (Why is no real title available?) | 2005-04-04 | Paper |
| scientific article; zbMATH DE number 2110623 (Why is no real title available?) | 2004-10-26 | Paper |
An arithmetic for non-size-increasing polynomial-time computation
Theoretical Computer Science | 2004-08-06 | Paper |
| scientific article; zbMATH DE number 2006627 (Why is no real title available?) | 2003-11-23 | Paper |
Term rewriting for normalization by evaluation.
Information and Computation | 2003-08-19 | Paper |
| scientific article; zbMATH DE number 1552509 (Why is no real title available?) | 2003-07-29 | Paper |
Refined program extraction from classical proofs
Annals of Pure and Applied Logic | 2002-09-16 | Paper |
| scientific article; zbMATH DE number 1390026 (Why is no real title available?) | 2002-01-31 | Paper |
| Refined program extraction from classical proofs: Some case studies | 2001-10-21 | Paper |
The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
Journal of Automated Reasoning | 2001-02-18 | Paper |
Higher type recursion, ramification and polynomial time
Annals of Pure and Applied Logic | 2000-09-04 | Paper |
| scientific article; zbMATH DE number 1497485 (Why is no real title available?) | 2000-08-28 | Paper |
Finite notations for infinite terms
Annals of Pure and Applied Logic | 2000-05-09 | Paper |
Monotone majorizable functionals
Studia Logica | 1999-10-28 | Paper |
| scientific article; zbMATH DE number 1342248 (Why is no real title available?) | 1999-09-22 | Paper |
Termination of permutative conversions in intuitionistic Gentzen calculi
Theoretical Computer Science | 1999-01-12 | Paper |
| scientific article; zbMATH DE number 1169381 (Why is no real title available?) | 1998-06-25 | Paper |
| scientific article; zbMATH DE number 1163991 (Why is no real title available?) | 1998-06-11 | Paper |
| scientific article; zbMATH DE number 1070627 (Why is no real title available?) | 1997-10-07 | Paper |
| scientific article; zbMATH DE number 806754 (Why is no real title available?) | 1997-06-15 | Paper |
| scientific article; zbMATH DE number 949290 (Why is no real title available?) | 1996-11-25 | Paper |
| scientific article; zbMATH DE number 785043 (Why is no real title available?) | 1995-09-26 | Paper |
| scientific article; zbMATH DE number 663929 (Why is no real title available?) | 1995-01-05 | Paper |
| scientific article; zbMATH DE number 432701 (Why is no real title available?) | 1993-11-11 | Paper |
| scientific article; zbMATH DE number 408809 (Why is no real title available?) | 1993-09-06 | Paper |
An upper bound for reduction sequences in the typed \(\lambda\)-calculus
Archive for Mathematical Logic | 1991-01-01 | Paper |
| scientific article; zbMATH DE number 4068861 (Why is no real title available?) | 1987-01-01 | Paper |
| scientific article; zbMATH DE number 3853066 (Why is no real title available?) | 1983-01-01 | Paper |
| scientific article; zbMATH DE number 3853055 (Why is no real title available?) | 1982-01-01 | Paper |
On bar recursion of types 0 and 1
Journal of Symbolic Logic | 1979-01-01 | Paper |
| scientific article; zbMATH DE number 3677794 (Why is no real title available?) | 1979-01-01 | Paper |
Definierbare Funktionen imλ-Kalkül mit Typen
Archiv für Mathematische Logik und Grundlagenforschung | 1976-01-01 | Paper |
| scientific article; zbMATH DE number 3497886 (Why is no real title available?) | 1975-01-01 | Paper |
| scientific article; zbMATH DE number 3531365 (Why is no real title available?) | 1975-01-01 | Paper |
Beweistheoretische Charakterisierung einer Erweiterung der Grzegorczyk-Hierarchie
Archiv für Mathematische Logik und Grundlagenforschung | 1972-01-01 | Paper |
Bemerkungen zum Spektralproblem
Mathematical Logic Quarterly | 1972-01-01 | Paper |
Eine Klassifikation der ε0‐Rekursiven Funktionen
Mathematical Logic Quarterly | 1971-01-01 | Paper |
Rekursionszahlen und die Grzegorczyk-Hierarchie
Archiv für Mathematische Logik und Grundlagenforschung | 1969-01-01 | Paper |
