I am a Ph.D. candidate in the Theoretical Computer Science section of the Vrije Universiteit Amsterdam, Netherlands. My Ph.D. is part of the Matryoshka project, where I work on extending the superposition calculus to higher-order logic. My Ph.D. supervisor is Jasmin Christian Blanchette. Before my Ph.D., I studied mathematics and computational linguistics.

**Email: **a.bentkamp☺vu.nl

**Phone: **+31 20 598 5849

**Address: **

Vrije Universiteit Amsterdam

Department of Computer Science

Section Theoretical Computer Science

De Boelelaan 1081, 1081 HV Amsterdam, The Netherlands

Room: S414

**Superposition for lambda-free higher-order logic**

Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, and Uwe Waldmann.
Accepted at *9th International Joint Conference on Automated Reasoning (IJCAR 2018)*.

Draft paper (PDF) ⋅
Draft report (PDF) ⋅
Slides (PDF) ⋅
Supplementary material

**A formal proof of the expressiveness of deep learning**

Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow.
Accepted at *8th Conference on Interactive Theorem Proving (ITP 2017)*.

Postprint (PDF) ⋅
Slides (PDF)

**An Isabelle formalization of the expressiveness of deep learning (extended abstract)**

Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. Accepted at *2nd Conference on Artificial Intelligence and Theorem Proving (AITP 2017)*.

Abstract (PDF) ⋅
Slides (PDF)

**An Isabelle formalization of the expressiveness of deep learning**

Alexander Bentkamp. M.Sc. thesis, Universität des Saarlandes, 2016.

Thesis (PDF)

**Expressiveness of deep learning**

Alexander Bentkamp. In Klein, G., Nipkow, T., Paulson, L. (eds.), *Archive of Formal Proofs*, 2016.

Formal proof development

**Latin Square**

Alexander Bentkamp. In Klein, G., Nipkow, T., Paulson, L. (eds.), *Archive of Formal Proofs*, 2016.

Formal proof development

I taught the exercise classes for Advanced Logic 2017/2018.