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