Alexander Bentkamp

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. My PhD supervisor is Jasmin Christian Blanchette. Before my PhD, 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

Publications:

A formal proof of the expressiveness of deep learning
Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. Accepted in Journal of Automated Reasoning.
Web page ⋅ Preprint (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)

Thesis:

An Isabelle formalization of the expressiveness of deep learning
Alexander Bentkamp. M.Sc. thesis, Universität des Saarlandes, 2016.
Thesis (PDF)

Formal proof developments:

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

Teaching:

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