Alexander P. Kreuzer's homepage

I am a machine learning/artificial intelligence professional with a strong background in theoretical computer science and mathematical logic.

Below you can find information on my research. My primary research interest are proof theory, computability theory, and formal methods.

Until July 2016 I was a research fellow in the mathematics department of National University of Singapore working together with Chi Tat Chong, Frank Stephan, and Yang Yue.

Prior to that I was a postdoc in the Plume team at Laboratoire de l'Informatique du Parallélisme, École normale supérieure de Lyon under Colin Riba and Alexandre Miquel.

I received my PhD in April 2012 from the Mathematics Department of Technische Universität Darmstadt under the supervision of Prof. Ulrich Kohlenbach.

Contact:

Email: matkaps [at] posteo [dot] de

Publications:

On the Uniform Computational Content of the Baire Category Theorem (with Vasco Brattka, and Matthew Hendtlass).
Final version in: Notre Dame Journal of Formal Logic, vol. 59 (2018), no. 4, pp. 605-636.
Preprint available at arXiv:1510.01913.
[doi:10.1215/00294527-2018-0016]
On the Uniform Computational Content of Computability Theory (with Vasco Brattka, and Matthew Hendtlass).
Final version in: Theory of Computing Systems 61 (2017), 1376.
Preprint available at arXiv:1501.00433.
[doi:10.1007/s00224-017-9798-1]
Measure theory and higher order arithmetic.
Final version in: Proc. Amer. Math. Soc. 143 (2015), 5411-5425.
Preprint available at arXiv:1312.1531.
[doi:10.1090/proc/12671] [MR 3411156]
Bounded variation and the strength of Helly's selection theorem.
Final version in: LMCS Vol. 10(4:16) 2014.
[doi:10.2168/LMCS-10(4:16)2014] [MR 3296477]
On principles between Σ1- and Σ2-induction, and monotone enumerations (with Keita Yokoyama).
Final version in: J. of Mathematical Logic 16, 1650004 (2016).
Preprint available at arXiv:1306.1936.
[doi:10.1142/S0219061316500045]
Minimal idempotent ultrafilters and the Auslander-Ellis theorem.
Preprint. arXiv:1305.6530.
Program extraction for 2-random reals.
Final version in: Archive for Mathematical Logic, vol. 52 (2013), no. 5-6, 659-666.
[doi:10.1007/s00153-013-0336-9] [MR 3072783]
On idempotent ultrafilters in higher-order reverse mathematics.
Final version in: J. of Symbolic Logic vol. 80 (2015), no. 1, pp. 179-193.
Preprint available at arXiv:1208.1424.
[doi:10.1017/jsl.2014.58] [MR 3320588]
A logical analysis of the generalized Banach contractions principle.
Final version in: Journal of Logic & Analysis, vol. 4 (2012), 17.
[MR 3002655]
From Bolzano-Weierstraß to Arzelà-Ascoli.
Final version in: Mathematical Logic Quarterly, vol. 60 (2014), no. 3, pp. 177-183
Preprint available at arXiv:1205.5429.
[doi:10.1002/malq.201200076] [MR 3207207]
Non-principal ultrafilters, program extraction and higher order reverse mathematics.
Final version in: J. of Mathematical Logic, vol. 12 (2012), no 1.
Preprint available at arXiv:1109.4277. Updated preprint.
[doi:10.1142/S021906131250002X] [MR 2950192]
On the strength of weak compactness.
Final version in: Computability, vol. 1 (2012), no. 2, 171-179.
Preprint available at arXiv:1106.5124. Updated preprint.
[doi:10.3233/COM-12010] [MR 3064228]
Primitive recursion and the chain antichain principle.
Final version in: Notre Dame J. Formal Logic, vol. 53 (2012), no. 2, 245-265.
[doi:10.1215/00294527-1715716] [MR 2925280]
Term extraction and Ramsey's theorem for pairs (with Ulrich Kohlenbach).
Final version in: J. of Symbolic Logic vol. 77 (2012), no. 3, pp. 853-895.
[doi:10.2178/jsl/1344862165] [MR 2987141]
The cohesive principle and the Bolzano-Weierstraß principle.
Final version in: Mathematical Logic Quarterly, vol. 57 (2011), no. 3, pp. 292-298.
Preprint available at arXiv:1005.5316.
[doi:10.1002/malq.201010008] [MR 2839129]
Ramsey's Theorem for pairs and provably recursive functions (with Ulrich Kohlenbach).
Final version in: Notre Dame Journal of Formal Logic, vol. 50 (2009), no. 4, pp. 427-444.
[doi:10.1215/00294527-2009-019] [MR 2598872]

Proof-mining and combinatorics: Program extraction for Ramsey's theorem for pairs.
PhD Thesis, May 2012.
Der Satz von Ramsey für Paare und beweisbar rekursive Funktionen.
Diploma Thesis (in German) supervised by Ulrich Kohlenbach, February 2009.

Research notes et cetera:

A lower bound on Gowers' FIN_k theorem. arXiv:1510.01838.
I have some code at GitHub. For instance a formal proof of Feteke's Lemma in LEAN.

Talks:

Reflection and the fine structure theorem. [SLIDES]
Talk at the Workshop on New Challenges in Reverse Mathematics, Institute for Mathematical Sciences, Singapore, January, 2016.
On the Uniform Computational Content of the Baire Category Theorem. [SLIDES]
Talk at the Dagstuhl Seminar 15392, September 2015.
On the Uniform Computational Content of Computability Theory. [SLIDES]
Invited Talk at the Conference on Computability and Complexity in Analysis 2015, Tokyo, July 2015.
On iteration principles between Σ1- and Σ2-induction.
Contributed talk at the Asian Logic Conference, Mumbai, India, January 2015.
Non-principal ultrafilters, program extraction and higher order reverse mathematics.
Talk at the IMS-JSPS Joint Workshop in Mathematical Logic and Foundations of Mathematics, Singapore, September 2014.
Measure theory and higher order arithmetic.
Talk at the Workshop on Computability Theory 2014, Prague, Czech Republic, July 2014.
Non-principal ultrafilters, program extraction and higher order reverse mathematics. [SLIDES]
Talk at the Mathematical Structures of Computation - Week 1 - Recent Developments in Type Theory, Lyon, France, January 2014.
Non-principal ultrafilters, program extraction and higher order reverse mathematics. [SLIDES]
Talk at the GdT Théorie des types et réalisabilité of Laboratoire Preuves, Programmes et Systémes at Université Paris 7, December 2013.
Non-principal ultrafilters, program extraction and higher order reverse mathematics. [SLIDES]
Talk at the Seminar Logic and Theoretical Computer Science of the Universität Bern, November 2013.
Bounded variation and Helly's selection theorem. [SLIDES]
Talk at the Seminar for Theoretical Computer Science and Mathematical Logic of the Universität der Bundeswehr, München, October 2013.
Program extraction and ultrafilters. [SLIDES]
Talk at the Special Session: Logical analysis of mathematical proofs of the Logic Colloquium 2013, Évora, Portugal, July 2013.
Abstract published in: Bull. Symbolic Logic 20, no. 2, p. 214 (2010).
Non-principal ultrafilters, program extraction and higher order reverse mathematics. [SLIDES]
Talk at the Workshop on Reverse Mathematics and Type Theory, Seoul, Korea, March 2013.
Non-principal ultrafilters, program extraction and higher order reverse mathematics. [SLIDES]
Talk at Chocola November 2012, Lyon, France.
Non-principal ultrafilters, program extraction and higher order reverse mathematics. [SLIDES]
Invited talk at the PhD Colloquium of the Colloquium Logicum 2012, Paderborn, Germany, September 2012.
Non-principal ultrafilters, program extraction and higher order reverse mathematics. [SLIDES]
Contributed talk at the Logic Colloquium 2012, Manchester, UK, July 2012.
From Bolzano-Weierstraß to Arzelà-Ascoli. [SLIDES]
Informal presentation at Continuity, Computability, Constructivity - From Logic to Algorithms '12, Trier, Germany, May 2012.
Program extraction and Ramsey's theorem for pairs. [SLIDES]
Talk at the Oberwolfach Workshop 1145: Mathematical Logic: Proof Theory, Constructive Mathematics, November 2011.
Abstract published in: Oberwolfach Report No. 52/2011.
The Bolzano-Weierstraß principle and the cohesive principle. [SLIDES]
Talk at the Dagstuhl Seminar 11411: Computing with Infinite Data, October 2011.
Abstract published in: Dagstuhl Report, Volume 1, Issue 10.
The cohesive principle and the Bolzano-Weierstraß principle. [SLIDES]
Informal presentation at the CiE 2011, Sofia, Bulgaria, June-July 2011.
Ramsey's Theorem for pairs and term extraction. [SLIDES]
Talk at the "RaTLoCC 2011 - Ramsey Theory in Logic, Combinatorics and Complexity", Bertinoro, Italy, May 2011.
Ramsey's theorem for pairs and program extraction. [SLIDES]
Talk at the AMS-ASL Special Session on Logic and Analysis at the Joint Mathematics Meetings, New Orleans, January 2011.
Abstract published in: Abstracts of Papers Presented to the Amer. Math. Soc. vol. 32, no. 1, issue 163, p. 15 (2011).
Ramsey's Theorem for pairs and provably recursive functions. [SLIDES]
Talk at the "RaTLoCC 2009 - Ramsey Theory in Logic, Combinatorics and Complexity", Bertinoro, Italy, October 2009.
Ramsey's Theorem for pairs and provably recursive functions. [SLIDES]
Contributed talk at the ASL Logic Colloquium, Sofia, Bulgaria, August 2009.
Abstract published in: Bull. Symbolic Logic 16, no. 1, p. 121 (2010).

Teaching at National University of Singapore:

2015/2016, Semester 1: MA5219 Logic and Foundations of Mathematics.

Teaching at TU Darmstadt:

Summer term 2012: Assistant for Formale Grundlagen der Informatik I+II [LINK I] [LINK II] (Foundations of computer science: automata theory and logic).
Summer term 2011: Assistant for Formale Grundlagen der Informatik I+II (Foundations of computer science: automata theory and logic).
Summer term 2010: Assistant for Formale Grundlagen der Informatik I+II (Foundations of computer science: automata theory and logic).