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.