Professor of Mathematics
Research Group Logic
Department
of Mathematics
Technische Universität
Darmstadt
Schlossgartenstrasse 7
D-64289 Darmstadt, Germany
kohlenbach [at] mathematik [dot] tu-darmstadt [dot] de
Tel.: (+49) 06151-16-22862 (Office)
Tel.: (+49) 06151-16-22863 (Secretary)
Fax: (+49) 06151-16-22840
I obtained my PhD (Dr.phil.nat.) in 1990 from the
Department of Mathematics
of the
J.W.Goethe-Universitaet Frankfurt (Germany).
In 1995 I got my Habilitation (`venia legendi') from the Department
of Mathematics of the University of Frankfurt.
During the academic year 1996-97 I was a visiting assistant professor
in the Department of
Mathematics of the University
of Michigan, Ann
Arbor. In July 1997, I joined BRICS
and the Department of Computer
Science of Aarhus
University (Aarhus, Denmark) where I became tenured associate professor
in 2000. Since April 2004
I am full professor of mathematics at Technische Universität
Darmstadt.
Research Interests: Logic (in particular proof theory, computability theory and constructive reasoning) with applications to mathematics and computer science, computational content of proofs, proof interpretations and their use in mathematics, functionals of higher type, approximation theory, nonlinear analysis, fixed point theory, ergodic theory, abstract Cauchy problems, convex feasibility problems.
Here is my Curriculum Vitae: CV.pdf.Current teaching (summer term 2024):
Editorial Work:
Other professional activities:
Wissenschaftliche Gesellschaft an der J.W.Goethe-Universität zu Frankfurt am Main (Member)
PhD Students:
Publications:
Book: Ulrich Kohlenbach: "Applied Proof Theory: Proof Interpretations and their Use in Mathematics". Springer Monographs in Mathematics, xx+536pp., 2008. Articles:Majorizable functionals and recursion theoretical models for W. Friedrichs calculi of functionals (german). Master thesis. Frankfurt 1986, pp. 91.
Theory of majorizable and continuous functionals and their use for the extraction of bounds from non-constructive proofs: effective moduli of uniqueness for best approximations from ineffective proofs of uniqueness (german). PhD Dissertation, Frankfurt 1990, pp.xxii+278.
Pointwise hereditary majorization and some application.. Final version in: Arch. Math. Logic 31, pp. 227-241 (1992).
Remarks on Herbrand normal forms and Herbrand realizations. Final version in: Arch. Math. Logic 31, pp. 305-317 (1992).
Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization. J. Symbolic Logic 57, pp. 1239-1273 (1992).
Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallee Poussin's proof for Chebycheff approximation. Final version in: Annals of Pure and Applied Logic 64, pp. 27-94 (1993).
New effective moduli of uniqueness and uniform a-priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory. Final version in: Numer.Funct.Anal.and Optimiz. 14, pp. 581-606 (1993).
A note on the $\Pi^0_2$-induction rule. Final version in: Arch. Math. Logic 34, pp. 279-283 (1995).
Real growth in standard parts of analysis. Habilitationsschrift, pp. xv+166, Frankfurt 1995.
Analysing proofs in analysis. Final version in: W. Hodges, M. Hyland, C. Steinhorn, J. Truss, editors, Logic: from Foundations to Applications. European Logic Colloquium (Keele, 1993), pp. 225-260, Oxford University Press (1996).
Mathematically strong subystems of analysis with low rate of growth of provably recursive functionals. Final version in: Arch. Math. Logic 36, pp. 31-71 (1996).
Elimination of Skolem functions for monotone formulas in analysis. Final version in: Arch. Math. Logic 37 pp. 363-390 (1998).
Arithmetizing proofs in analysis. Final version in: Larrazabal, J.M., Lascar, D., Mints, G. (eds.), Logic Colloquium '96, Springer Lecture Notes in Logic 12, pp. 115-158 (1998).
Proof theory and computational analysis. Electronic Notes in Theoretical Computer Science, Vol. 13, Elsevier (1998).
Relative constructivity. Final version in: J. Symbolic Logic 63, pp. 1218-1238 (1998).
On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness. Final version in: Ann. Pure Applied Logic 95, pp. 257-285 (1998).
The use of a logical principle of uniform boundedness in analysis. Final version in: Cantini, A., Casari, E., Minari, P. (eds.), Logic and Foundations of Mathematics. Synthese Library 280, pp. 93-106. Kluwer Academic Publishers (1999).
A note on Goodman's theorem. Final version in: Studia Logica 63, pp. 1-5 (1999).
On the no-counterexample interpretation. Final version in: J. Symbolic Logic 64, pp. 1491-1511 (1999).
Things that can and things that can't be done in PRA. Final version in: Ann. Pure Applied Logic 102, pp. 223-245 (2000).
A note on Spector's quantifier-free rule of extensionality. Final version in: Arch. Math. Logic 40, pp. 89-92 (2001).
On the computational content of the Krasnoselski and Ishikawa fixed point theorems. Final version in: Proceedings of the Fourth Workshop on Computability and Complexity in Analysis, J. Blanck, V. Brattka, P. Hertling, K. Weihrauch (eds.), Springer LNCS 2064, pp. 119-145 (2001).
Intuitionistic choice and restricted classical logic. Final version in: Math. Logic Quaterly 47, pp. 455-460 (2001).
A quantitative version of a theorem due to Borwein-Reich-Shafrir. Final version in: Numer. Funct. Anal. and Optimiz. 22, pp. 641-656 (2001).
On uniform weak König's lemma. Final version in: Ann. Pure Applied Logic 114, pp. 103-116 (2002).
Foundational and mathematical uses of higher types. Final version in: Sieg, W. et al. (eds.), Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman. Lecture Notes in Logic vol. 15, pp. 92-116, A.K. Peters (2002).
On weak Markov's principle. Final version in: Math. Logic Quaterly 48, suppl 1, pp. 59-65 (2002).
Applied foundations: proof mining in analysis. Final version in: Newsletter of the Danish Mathematical Society (`Matilde'), vol. 13, pp. 7-9 (2002).
Proof mining in L_1-approximation (with Paulo Oliva). Final version in: Ann. Pure Applied Logic 121, pp. 1-38 (2003).
Uniform asymptotic regularity for Mann iterates. Final version in: J. Math. Anal. Appl. 279, pp. 531-544 (2003).
Mann iterates of directionally nonexpansive mappings in hyperbolic spaces (with Laurentiu Leustean). Final version in: Abstract and Applied Analysis, vol. 2003, no.8, pp. 449-477 (2003).
Proof mining: a systematic way of analysing proofs in mathematics (with Paulo Oliva). Final version in: Proc. Steklov Inst. Math., vol. 242, pp. 136-164 (2003).
Bounds on iterations of asymptotically quasi-nonexpansive mappings(with Branimir Lambov). Final version in: Falset, J.G., Fuster, E.L., Sims, B. (eds.), Proc. International Conference on Fixed Point Theory and Applications, Valencia 2003, pp. 143-172, Yokohama Publishers (2004)
An arithmetical hierarchy of the law of excluded middle and related principles (with Yohji Akama, Stefano Berardi and Susumu Hayashi). In: Proc. of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), pp. 192-201, IEEE Press (2004). Erratum
Some logical metatheorems with applications in functional analysis. Final version in: Trans. Amer. Math. Soc. vol. 357, no. 1, pp. 89-128 (2005).
A complexity analysis of functional interpretations(with Mircea-Dan Hernest). Final version in: Theoretical Computer Science vol. 338, pp. 200-246 (2005).
Higher order reverse mathematics. Final version in: Stephen G. Simpson (ed.) Reverse Mathematics 2001. Lecture Notes in Logic vol. 21, pp. 281-295. ASL, A K Peters (2005).
Extracting Herbrand disjunctions by functional interpretation(with Philipp Gerhardy). Final version in: Arch. Math. Logic. vol. 44, pp. 633-644 (2005).
Some computational aspects of metric fixed point theory. Final version in: Nonlinear Analysis vol. 61, no. 5, pp. 823-837 (2005).
Strongly uniform bounds from semi-constructive proofs(with Philipp Gerhardy). Final version in: Ann. Pure Applied Logic vol. 141, pp. 89-107 (2006).
A logical uniform boundedness principle for abstract metric and hyperbolic spaces. Final version in: Electronic Notes in Theoretical Computer Science vol. 165 (Proc. WoLLIC 2006), pp. 81-93 (2006).
The approximate fixed point property in product spaces(with Laurentiu Leustean). Final version in: Nonlinear Analysis vol. 66, pp. 806-818 (2007).
Shoenfield is Goedel after Krivine (with Thomas Streicher). Final version in: Math. Logic Quaterly vol. 53, pp. 176-179 (2007).
Proof interpretations and the computational content of proofs in mathematics. Final version in: Bulletin EATCS no.93, pp. 143-173 (2007).
Effective bounds from proofs in abstract functional analysis. Final version in: Cooper, B., Loewe, B., Sorbi, A. (eds.), New Computational Paradigms: Changing Conceptions of What is Computable. Springer Publisher, pp. 223-258 (2008).
Interview on the Philosophy of Mathematics. Final version in: Philosophy of Mathematics: 5 Questions. Henricks, V.F., Leitgeb, H. (eds.), Automatic Press/VIP, pp. 183-190, 2008.
General logical metatheorems for functional analysis(with Philipp Gerhardy). Final version in: Trans. Amer. Math. Soc. 360, pp. 2615-2660 (2008).
Gödel's functional interpretation and its use in current mathematics. Final version in: Kurt Gödel and the Foundations of Mathematics. Horizons of Truth. Baaz, M. et al. (eds.), Cambridge University Press, New York, pp. 361-398, 2011. Reprinted in: dialectica Vol. 62, no. 2, pp. 223-267 (2008).
Herbrand's theorem and extractive proof theory. Final version in: SMF - Gazette des Mathematiciens 118, pp. 29-41, 2008.
A quantitative Mean Ergodic Theorem for uniformly convex Banach spaces (with Laurentiu Leustean). Final version in: Ergodic Theory and Dynamical Systems Vol. 29, pp. 1907-1915 (2009).
Ramsey's theorem for pairs and provably recursive functions (with Alexander Kreuzer). Final version in: Notre Dame Journal of Formal Logic vol. 50, pp. 427-444 (2009).
Asymptotically nonexpansive mappings in uniformly convex hyperbolic spaces (with Laurentiu Leustean). Final version in: Journal of the European Mathematical Society Vol. 12, pp. 71-92 (2010).
On Tao's "finitary" infinite pigeonhole principle (with Jaime Gaspar). Final version in: J. Symbolic Logic 75, pp. 355-371 (2010).
On the logical analysis of proofs based on nonseparable Hilbert space theory. Final version in: Feferman, S., Sieg, W. (eds.), `Proofs, Categories and Computations. Essays in Honor of Grigori Mints'. College Publications, pp. 131-143 (2010).
On the computational content of the Bolzano-Weierstrass principle (with Pavol Safarik). Final version in: Math. Logic Quaterly vol. 56, pp. 508-532 (2010).
On quantitative versions of theorems due to F.E. Browder and R. Wittmann. Final version in: Advances in Mathematics 226, pp. 2764-2795 (2011).
Effective rates of convergence for Lipschitzian pseudocontractive mappings in general Banach spaces (with Daniel Körnlein). Final version in: Nonlinear Analysis vol. 74, pp. 5253-5267 (2011).
A note on the monotone functional interpretation. Final version in: Math. Logic Quart. vol. 57, pp. 611-614 (2011).
On the asymptotic behavior of odd operators. Final version in: J. Math. Anal. Appl. vol. 382, pp. 615-620 (2011).
Gödel functional interpretation and weak compactness. Final version in: Ann. Pure Applied Logic vol. 163, pp. 1560-1579 (2012).
A uniform quantitative form of sequential weak compactness and Baillon's nonlinear ergodic theorem. Final version in: Communications in Contemporary Mathematics 14, 20pp. (2012).
Term extraction and Ramsey's theorem for pairs (with Alexander P. Kreuzer). Final version in: J. Symbolic Logic 77, pp. 853-895 (2012).
Effective metastability of Halpern iterates in CAT(0) spaces. (with Laurentiu Leustean). Final version in: Advances in Mathematics vol. 231, pp. 2526-2556 (2012). Addendum. (Final version in: Advances in Mathematics vol. 250, pp. 650-651, 2014)
On the computational content of convergence proofs via Banach limits (with Laurentiu Leustean). Final version in: Philosophical Transactions of the Royal Society A vol. 370, pp. 3449-3463 (2012).
Effective metastability for modified Halpern iterations in CAT(0) spaces (with Katharina Schade). Final version in: Fixed Point Theory and Applications 2012:191, 19pp.
Bounds on Kuhfittig's iteration schema in uniformly convex hyperbolic spaces (with Muhammad Aqeel Ahmad Khan). Final version in: J. Math. Anal. Appl. vol. 403, pp. 633-642 (2013).
Rate of metastability for Bruck's iteration of pseudocontractive mappings in Hilbert space (with Daniel Körnlein). Final version in: Numer. Funct. Anal. and Optimiz. vol. 35, pp. 20-31 (2014).
Fluctuations, effective learnability and metastability in analysis (with Pavol Safarik). Final version in: Ann. Pure and Applied Logic vol. 165, pp. 266-304 (2014).
Quantitative image recovery theorems (with Muhammad Aqeel Ahmad Khan). Final version in: Nonlinear Analysis vol. 106, pp. 138-150 (2014).
Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators (with Angeliki Koutsoukou-Argyraki). Final version in: J. Math. Anal. Appl. vol. 423, 1089-1112 (2015).
Classical provability of uniform versions and intuitionistic provability (with Makoto Fujiwara). Final version in: Math. Logic Quarterly vol. 61, pp. 132-150 (2015).
On the disjunctive Markov principle. Final version in: Studia Logica vol. 103, pp. 1313-1317 (2015).
Effective asymptotic regularity for one-parameter nonexpansive semigroups (with Angeliki Koutsoukou-Argyraki). Final version in: J. Math. Anal. Appl. vol. 433, pp. 1883-1903 (2016).
Logical metatheorems for abstract spaces axiomatized in positive bounded logic (with Daniel Günzel). Final version in: Advances in Mathematics vol. 290, pp. 503-551 (2016).
On the quantitative asymptotic behavior of strongly nonexpansive mappings in Banach and geodesic spaces. Final version in: Israel Journal of Mathematics vol. 216, pp. 215-246 (2016).
Quantitative asymptotic regularity for the composition of two mappings (with G. Lopez-Acedo and A. Nicolae). Final version in: Optimization vol. 66, pp. 1291-1299 (2017).
Recent progress in proof mining in nonlinear analysis. Final version in: IFCoLog Journal of Logics and their Applications, vol.10, Issue 4, pp. 3361-3410 (2017).
A proof-theoretic bound extraction theorem for CAT(κ)-spaces (with Adriana Nicolae). Final version in: Studia Logica vol. 105, pp. 611-624 (2017).
Quantitative results on Fejer monotone sequences (with Laurentiu Leustean and Adriana Nicolae). Final version in: Communications in Contemporary Mathematics vol. 20 (2018), 42pp., DOI: 10.1142/S0219199717500158.
Interrelation between weak fragments of double negation shift and related principles (with Makoto Fujiwara). Final version in: J. Symb. Logic vol. 83, pp. 991-1012 (2018).
On proximal mappings with Young functions in uniformly convex Banach spaces (With M. Bacak). Final version in: Journal of Convex Analysis 25, pp. 1291-1318 (2018).
Moduli of regularity and rates of convergence for Fejer monotone sequences (with Genaro Lopez-Acedo and Adriana Nicolae). Final version in: Israel Journal of Mathematics vol. 232, pp. 261-297 (2019).
A polynomial rate of asymptotic regularity for compositions of projections in Hilbert space. Final version in: Foundations of Computational Mathematics vol. 19, pp. 83-99 (2019).
Proof-theoretic Methods in Nonlinear Analysis. Final version in: Proc. ICM 2018, B. Sirakov, P. Ney de Souza, M. Viana (eds.), Vol. 2, pp. 61-82. World Scientific 2019.
On the reverse mathematics and Weihrauch complexity of moduli of regularity and uniqueness.Final version in: Computability vol. 8, pp. 377-387 (2019).
Local formalizations in nonlinear analysis and related areas and proof-theoretic tameness. Final version in: P. Weingartner and H.-P. Leeb (eds.), `Kreisel's Interests. On the Foundations of Logic and Mathematics'. College Publications. Tributes vol. 41, pp. 45-61, 2020.
Rates of convergence for iterative solutions of equations involving set-valued accretive operators (with Thomas Powell). Final version in: Computers & Mathematics with Applications vol. 80, pp. 490-503 (2020).
Quantitative analysis of a Halpern-type Proximal Point Algorithm for accretive operators in Banach spaces.. Final version in: Journal of Nonlinear and Convex Analysis vol. 21, no.9, pp. 2125-2138 (2020).
Quantitative results on the Proximal Point Algorithm in uniformly convex Banach spaces. Final version in: Journal of Convex Analysis vol. 28, No.1, pp. 11-18 (2021).
The finitary content of sunny nonexpansive retractions (with Andrei Sipos). Final version in: Communications in Contemporary Mathematics Vol. 23, No. 01, 1950093, 63pp. (2021).
A uniform betweenness property in metric spaces and its role in the quantitative analysis of the `Lion-Man' game (with Genaro Lopez-Acedo and Adriana Nicolae). Final version in: Pacific J. Math. Vol. 310, pp. 181-212 (2021).
Quantitative analysis of a subgradient-type method for equilibrium problems (with Nicholas Pischke). Final version in: Numerical Algorithms Vol. 90, pp. 197-219 (2022).
On the Proximal Point Algorithm and its Halpern-type variant for generalized monotone operators in Hilbert space. Final version in: Optimization Letters vol. 16, pp. 611-621 (2022).
Quantitative translations for viscosity approximation methods in hyperbolic spaces (with Pedro Pinto). Final version in: J. Math. Anal. Appl. vol. 507, 125823, 33 pages (2022).
R.E. Bruck, proof mining and a rate of asymptotic regularity for ergodic averages in Banach spaces(with Anton Freund). Final version in: Applied Set-Valued Analysis and Optimization vol.4, pp. 323-336 (2022).
Bounds for a nonlinear ergodic theorem for Banach spaces (with Anton Freund). Final version in: Ergodic Theory and Dynamical Systems, vol.43, pp. 1570-1593 (2023).
Kreisel's `shift of emphasis' and contemporary proof mining. Final version in: Studies in Logic Vol.16, No.3, pp. 1-35 (2023), see Studies in Logic.
Proof theory and nonsmooth analysis (with Nicholas Pischke). Final version in: Philosophical Transactions of the Royal Society A vol.381, Issue 2248, DOI 10.1098/rsta.2022.0015, 21 pages (2023).
On modified Halpern and Tikhonov-Mann iterations (with H. Cheval and L. Leustean). Final version in: Journal of Optimization Theory and Applications (JOTA), vol.197, pp. 233-251 (2023).
Rates of convergence and metastability for Chidume's algorithm for the approximation of zeros of accretive operators in Banach spaces (with Richard Findling). Final version in: Numerical Functional Analysis and Optimization, vol.45, pp.216-233 (2024).
Fejer monotone sequences revisited (with Pedro Pinto). Submitted
Effective rates for iterations involving Bregman strongly nonexpansive operators (with Nicholas Pischke). Submitted
On the computational content of moduli of regularity and their logical strength. Submitted.
Herbrand analyses in geometry: a case study (with Luisa Marie Despres). Submited.
Published abstracts in journals:
Constructions in classical analysis by unwinding proofs using majorizability (abstract). J. Symbolic Logic 57, p. 307 (1992).
Herbrand normal forms in subsystems of (second-order) arithmetic (abstract). J. Symbolic Logic 58, pp. 1148-1149 (1993).
Exploiting partial constructivity relatively to non-constructive lemmas in given proofs (abstract). Bull. Symbolic Logic 1, pp. 243-244 (1995).
Real growth in standard parts of analysis (abstract). Bull. Symbolic Logic 3, p. 104 (1997).
General logical principles of uniform boundedness and their mathematical strength (abstract). Bull. Symbolic Logic 3, p. 387 (1997).
Mathematically strong extensions of ACA$_0$ (abstract). Bull. Symbolic Logic 5, pp. 141-142 (1999).
On extensions of weak König's lemma (abstract). Bull. Symbolic Logic 6, p. 117 (2000).
Applied foundations: recent progress in proof mining. Abstract of Papers Presented to the Amer. Math. Soc. vol. 22, no. 3, issue 125, p. 436 (2001).
(with Paulo Oliva) Effective bounds on strong unicity in L1-approximation (abstract). Bull. Symbolic Logic 8, p. 143 (2002).
Proof theoretic applications to functional analysis (abstract). Bull. Symbolic Logic 10, pp. 122-123 (2004).
Recent uses of proof theory in nonlinear analysis and geodesic geometry. (abstract). Bull. Symbolic Logic 13, p.377 (2007).
Applied proof theory: Proof interpretations and their use in mathematics (abstract). Bull. Symbolic Logic 16, pp. 92-93 (2010).
Uniform bounds from proofs in nonlinear ergodic and fixed point theory. Abstract of Papers Presented to the Amer. Math. Soc. vol. 32, no. 1, issue 163, p.15 (2011).
Recent developments in proof mining: Bounds from proofs in nonlinear ergodic theory (abstract). Bull. Symbolic Logic 19, p.404 (2013).
Proof-theoretic metatheorems for metric structures and their relation to positive bounded logic (abstract). Bull. Symbolic Logic 23, p.366 (2017).
Proof-theoretic methods in convex optimization (abstract). Bull. Symbolic Logic 24, p. 508 (2018).
Local proof-theoretic foundations, proof-theoretic tameness and proof mining (abstract).Bull. Symbolic Logic 25, p.482 (2019).
Projects:
Principal investigator of DFG Project KO 1737/6-1: Proof Mining in Convex Optimization and Related Areas (April 2018-March 2021).
This project has been extended (KO 1737/6-2) until 2024.
Principal investigator of DFG Project KO 1737/5-1: Extraction of effective bounds from proofs based on sequential compactness via logical analysis (Feb 2009-Feb 2013).
This project has been extended (KO 1737/5-2) until November 2016.
Principal investigator of IRTG 1529 `Mathematical Fluid Dynamics' (Tokyo-Darmstadt), 2013-2018.
Member of Deutsch-Russisches Kooperationsprojekt "Berechnungen ueber nichtdiskreten Strukturen: Modelle, Semantik, Komplexität" (DFG 436 RUS 113/850/0-1), 2006-2008.
Member of Deutsch-Südafrikanisches Kooperationsprojekt "From continuity to computability, (DFG/NRF 445 SUA-113/20/0-1), 2007-2009.
Member of APSEM II (IST-2001-38957 Programme of EU.
Principal investigator of project of the Danish Natural Science Research Council (Sagsnr.: 21-02-0474) "Proof Mining: A Logical Approach to Computational Mathematics (2003-2005; stopped in April 2004 due to my move to Germany).
Member of Board of BRICS International PhD School, Dept. of Computer Science, Aarhus University 2000-2004.
Link to the International Research Training Group 1529: Mathematics Fluid Dynamics.
HOT SPOTS:
Colloquium Logicum 2024, Vienna 7-9 October 2024.
Workshop on Proof Mining 2024, TU Darmstadt, 4-6 September 2024.
Logic Colloquium 2024, U Gothenburg (Sweden), June 24-28, 2024.
Conference on Techniques from Logic in Mathematics, TU Vienna, December 7, 2023.
Working Formal Methods Symposium (FROM 2023), Bucharest, September 21-22, 2023.
Applied Proof Theory, U Chieti-Pescara, Italy, August 29-September 2, 2022.
Proof and Computation 2022, May 30- June 2, 2022, Schlehdorf monastery.
New Directions in Computability Theory, CIRM Luminy, March 7-11, 2022.
Logical Perspectives 2021, Moscow, June 7-11, 2021. Held online.
IECMSA-2020, Skopje, North Macedonia, August 25-28, 2020. Held online.
Anne Troelstra Memorial Event 2020, Amsterdam, March 6, 2020.
ASL Logic Colloquium, August 11-16, 2019, Prague.
Proof, Computation, Complexity. Institut Mittag-Leffler, July 15-19, 2019, Djursholm.
Conference on Mathematical Logic. Niteroi, Brazil, Aug 10-11, 2018.
International Congress of Mathematicians 2018 (ICM 2018), Rio, August 1-9, 2018.
HIM Trimester Program: Types, Sets and Constructions, HIM Bonn, May 2- Aug 24, 2018.
AAA96 - 96. Arbeitstagung Allgemeine Algebra. TU Darmstadt. June 1-3, 2018.
ASL 2018 North American Annual Meeting. May 16-19, 2018, Macomb (IL), USA.
Computational Approaches to the Foundations of Mathematics. LMU Munich, April 11-13, 2018.
Oberwolfach Workshop on Computability. Mathematical Research Institute Oberwolfach, Jan. 7-13, 2018.
Autumn school "Proof and Computation", Sep. 23-26, 2017, Herrsching, Germany.
Computability Theory. Dagstuhl Seminar, February 19-24, 2017.
Hilbert Bernays Summer School on Logic and Computation, U Göttingen, July 25-29, 2016.
PhDs in Logic 2016, Darmstadt, May 9-11.
New Challenges in Reverse Mathematics, January 3-16, 2016, Singapore.
12th International Seminar on Optimization and Related Areas. October 5-9, 2015, Lima, Peru.
Utrecht Workshop on Proof Theory, April 16-18, 2015.
WoLLIC 2014, Valpariaso, Chile, Sep. 1-4.
IRTG 1529 Kickoff Meeting, Waseda University, Tokyo, Japan, June 17-18, 2014.
IRTG 1529 Research Seminar "Proof Mining and Nonlinear Analysis", TU Darmstadt, Feb. 26-28, 2014.
Universality and Homogeneity. Hausdorff Trimester Program September 2 - December 20, 2013, Bonn.
Humboldt-Kolleg "Proof", Bern, Sep. 9-13, 2013.
Honory doctorate for Prof. Dr. Harvey M. Friedman and affiliated workshop, U Gent, Sep. 4-5, 2013.
WoLLIC 2013, TU Darmstadt, August 20-23
Proof Theory in Lisbon, July 19, 2013.
Types 2013, Toulouse, April 23-26, 2013.
3rd Workshop on Proof Theory and Rewriting. Kanazawa (Japan), March 4-8, 2013.
COLD SPOTS:
Third MALOA Training Workshop, University of Oxford, Mathematical Institute, Aug.26 - Sep.1, 2012.
15th Latin American Symposium on Mathematical Logic Bogotá, Colombia, June 4-8, 2012.
Workshop on Proof Theory and Computability Theory, Tokyo, Feb. 20-23, 2012.
Ramsey Theory in Logic, Combinatorics and Complexity. Bertinoro (Italy), May 22-27, 2011.
AMS-ASL Special Session on Logic and Analysis. New Orleans, January 6-9, 2011.
Collegium Logicum: Proofs and Structures, Paris, November 8-10, 2010.
Colloquium Logicum 2010 of the DVMLG. WWU Münster, September 22-24, Germany, 2010.
Colloquium PhD's in Logic II. Tilburg University, February 18-19, 2010, The Netherlands.
Reverse Mathematics: Foundations and Applications, University of Chicago, November 6-8, 2009.
Workshop on Ergodic Theory, Queen Mary, University of London London UK, October 30, 2009.
Maltsev Meeting, Novosibirsk, 24-28 August 2009.
Logic and Mathematics Conference, University of York, 3-7 August 2009.
ASL Logic Colloquium 2009, Sofia, Bulgaria, July 31- August 5, 2009.
Leeds Symposium on Proof Theory and Constructivism, Leeds, UK, July 3-16, 2009.
Computability, Reverse Mathematics and Combinatorics, December 7-12, Banff (Canada), 2008.
Colloquium Logicum 2008, TU Darmstadt, September 10-12. 2008
British Logic Colloquium 2008, September 4-6, 2008, University of Nottingham.
Centenary Paul Wolfskehl (with Andrew Wiles), TU Darmstadt, June 30, 2008.
Mathematical Logic: Proof Theory, Constructive Mathematics. Obwerwolfach, April 6-12, 2008
L'Heritage Scientifique de Jacques Herbrand. Herbrand Centenary, February 15, 2008, ENS, Paris.
Workshop "Deduction in Semantics", Stuttgart, 10.-12.10.2007.
ASL Logic Colloquium 2007, Worclaw. July 14-19, 2007.
2006-2007 ASL Winter Meeting. January 7-8, New Orleans, USA.
Computer Science Logic 2006 (CSL 2006), 25-29 September, 2006, Szeged, Hungary.
Minisymposium on "The use of proof theory in mathematics" within the DMV 2006 Meeting, Bonn 17.-23.09.06.
MAP 2006, Castro Urdiales (Spain), 9.1.2006-13.1.2006.
CSL'05, Oxford, UK, 22-25 August 2005.
Tagung: Logik und Wissen, Darmstadt 24.-26. Juni 2005
Computability in Europe 2005: New Computational Paradigms ILLC (Amsterdam), June 8-12, 2005
Logic Meeting at UCLA to inaugurate the UCLA Logic Center, February 3-6, 2005.
Computability in Analysis. Kyushu University, Fukuoka, Nov. 22-26, 2004.
Jahrestagung der Deutschen Mathematiker- Vereinigung, Heidelberg, Sept. 12-17, 2004
Sixth
International Workshop on Computability and Complexity in Analysis,
Wittenberg, Germany, August 16-20, 2004
2003
ASL Annual Meeting
University of Illinois at Chicago, Chicago, Illinois
June 1-4, 2003
18th IEEE Conference
on Computational Complexity, BRICS, University of Aarhus, Denmark,
July 7-10, 2003
International
Conference of Fixed Point Theory and Applications, Valencia (Spain),
July 13-19, 2003
12th. International
Congress of Logic Methodology and Philosophy of Science, Oviedo
(Spain), August 7-13, 2003
Symposium
on `Unusual
Effectiveness of Logic in Computer Science', Oviedo 2003 (as part of
LMPS)
Fall school of
the Logic seminar of the Mathematical Institute of the
Academy of Sciences of the Czech Republic, Pec p. Snezkou,
Sept. 14-20,
2003.
Workshop
on Proof Theory and Algorithms, Edinburgh, March
23-29, 2003
2002 Computability on the Continuuum Seminar, Kyoto, December 14-16, 2002
CSL'02: Annual Conference
of the European Association for Computer Science Logic, Edinburgh,
September 22-25, 2002
FLoC'02: The 2002 Federated Logic Conference,
Copenhagen, Denmark, July 20 -- August 1, 2002
As part of FLoC'02:
Seventeenth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS
2002), July 22-25, 2002 Copenhagen.
Bounded
Systems and Computational Complexity, Lisbon, June 28-29, 2002.
Meeting of
the American Mathematical Society, Columbus (Ohio), September 21-23,
2001
EEF Summer School
on Logical Methods, Aarhus, Denmark, June 25-July 6, 2001
International Conference
MATHEMATICAL LOGIC, ALGEBRA AND SET THEORY (dedicated to the
100 anniversary of P.S. Novikov), Moscow, August 27-31, 2001
Fourth Workshop on Computability and Complexity in Analysis, September
17-19, 2000, Swansea, Wales
Series of lectures
on Constructive Mathematics by D.S. Bridges, Roskilde and Aarhus,
Aug 30- Sep 1
Summer School on
"Philosophy of Mathematics", University of Roskilde, June 19-32, 2000,
Roskilde
Memorial
Colloquium for Professor Kurt Schuette and Workshop `Proof and Computation'
(November 5-6, 1999)
First St. Petersburg Days
of Logic and Computability (May 26-29, 1999)
Reflections: A Symposium Honoring Solomon Feferman on his 70th Birthday
(December 11-13, 1998, Stanford University)
BRICS THEME '98: Proofs and Complexity
BRICS
Workshop: Proof Theory and Complexity (August 3-7, 1998)