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. I am also collaborating with the Lean Forward project. My PhD supervisor is Jasmin Blanchette. Before my PhD, I studied mathematics and computational linguistics.

Email: a.bentkampvu.nl

Phone: +31 20 598 4221

Address:
Vrije Universiteit Amsterdam
Department of Computer Science
Section Theoretical Computer Science
De Boelelaan 1081, 1081 HV Amsterdam, The Netherlands
Room: T-454


Publications:

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.
Preprint (PDF)Report (PDF)Slides (PDF)

A formal proof of the expressiveness of deep learning
Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. Accepted in Journal of Automated Reasoning.
Web pagePreprint (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 pagePostprint (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 pagePostprint (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 exercise classes for Advanced Logic 2017/18 and Logical Verification 2018/19.