I am a PhD candidate in the Theoretical Computer Science section of the Vrije Universiteit Amsterdam, Netherlands. My PhD is part of the Matryoshka project, where I work on extending the superposition calculus to higher-order logic. I am also collaborating with the Lean Forward project. My PhD supervisors are Jasmin Blanchette, Wan Fokkink, and Uwe Waldmann. Before my PhD, I studied mathematics and computational linguistics.

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

**Phone: **+31 20 598 9544

**Address: **

Vrije Universiteit Amsterdam

Department of Computer Science

Section Theoretical Computer Science

De Boelelaan 1111, 1081 HV Amsterdam, The Netherlands

Room: 12A71

**The Embedding Path Order for Lambda-Free Higher-Order Terms**

Alexander Bentkamp.

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

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

Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, and Uwe Waldmann.

Draft article (PDF) ⋅
Supplementary material

**Efficient full higher-order unification**

Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin.

Draft paper (PDF) ⋅
Draft report (PDF)

**Superposition with lambdas**

Alexander Bentkamp, Jasmin Christian Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann.
In Fontaine, P. (ed.) *27th International Conference on Automated Deduction (CADE-27)*, LNCS, Springer, 2019.

Web page ⋅
Postprint (PDF) ⋅
Report (PDF) ⋅
Slides (PDF)

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

Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. *Journal of Automated Reasoning* **63**(2), pp. 347-368, 2019.

Web page ⋅
Postprint (PDF)

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

Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, and Uwe Waldmann.
In Galmiche, D., Schulz, S., Sebastiani, R. (eds.) *9th International Joint Conference on Automated Reasoning (IJCAR 2018)*,
LNCS 10900, pp. 28–46, Springer, 2018.

Web page ⋅
Postprint (PDF) ⋅
Report (PDF) ⋅
Slides (PDF) ⋅
Supplementary material

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

Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow.
In Ayala-Rincón, M., Muños, C. A. (eds.) *8th Conference on Interactive Theorem Proving (ITP 2017)*,
LNCS 10499, pp. 46–64, Springer, 2017.

Web page ⋅
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)

**Embedding Path Order for Lambda-Free Higher-Order Terms**

Alexander Bentkamp. *Archive of Formal Proofs*, 2018.

Formal proof development

**Expressiveness of deep learning**

Alexander Bentkamp. *Archive of Formal Proofs*, 2016.

Formal proof development

**Latin Square**

Alexander Bentkamp. *Archive of Formal Proofs*, 2016.

Formal proof development

- Logical Verification 2019/20
- Logical Verification 2018/19 (Teaching assistant)
- Advanced Logic 2017/18 (Teaching assistant)