Alexander Bentkamp

I am a postdoctoral researcher at the Mathematical Institute of the Heinrich-Heine-Universität Düsseldorf. My main research interests are interactive and automated theorem proving. I have a PhD in computer science from the Vrije Universiteit Amsterdam.

alexander.bentkamphhu.de 0000-0002-7158-3595

News

Awards for My PhD Thesis

My thesis won the Ackermann Award, the Beth Award, the McCune Award, and the IPA dissertation award!

Thesis (PDF)
Zipperposition Won Trophy

Now for the third time in a row, Zipperposition won the higher-order division of the prover competition CASC.

CASC website
Mechanical Mathematicians

The article "Mechanical Mathematicians" has been accepted by the Communications of the ACM.

Preprint (PDF)

Publications:

Verified Reductions for Optimization
Alexander Bentkamp, Ramon Fernández Mir, Jeremy Avigad.
Accepted at the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023).
Preprint (PDF)

HHLPy: Practical Verification of Hybrid Systems using Hoare Logic
Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan.
Accepted at the International Symposium on Formal Methods 2023.
Preprint (PDF)

Superposition for Higher-Order Logic
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirović. Journal of Automated Reasoning 67: Article number: 10, 2021.
Publisher's pagePreprint (PDF)

Privacy accounting εconomics: Improving differential privacy composition via a posteriori bounds
Valentin Hartmann, Vincent Bindschaedler, Alexander Bentkamp, Robert West. Proceedings on Privacy Enhancing Technologies 2022(3): 222–246, 2022.
Publisher's pagePreprint (PDF)

An Impossible Asylum
Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, and Wojciech Nawrocki.
Accepted at The American Mathematical Monthly.
Preprint (PDF)

Mechanical Mathematicians
Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann.
Accepted at the Communications of the ACM.
Preprint (PDF)

Verified Optimization (work in progress)
Alexander Bentkamp and Jeremy Avigad. Accepted at the Workshop on Formal Mathematics for Mathematicians (FMM 2021).
Preprint (PDF)

Efficient full higher-order unification
Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin. Logical Methods in Computer Science 17(4): 18:1–18:31, 2021.
Publisher's pageAuthors' PDF

The Embedding Path Order for Lambda-Free Higher-Order Terms
Alexander Bentkamp. Journal of Applied Logics 8(10): 2447-2469, 2021.
Publisher's pageAuthors' PDFSupplementary materialSlides (PDF)

Superposition for full higher-order logic
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirović. In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28), LNCS, Springer, 2021.
Publisher's pageAuthors' PDFReport (PDF)Slides (PDF)

Superposition with first-class Booleans and inprocessing clausification
Visa Nummelin, Alexander Bentkamp, Sophie Tourret, and Petar Vukmirović. In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28), LNCS, Springer, 2021.
Publisher's pageAuthors' PDFReport (PDF)

Making Higher-Order Superposition Work
Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28), LNCS, Springer, 2021.
Publisher's pageAuthors' PDF

Superposition with lambdas
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann. Journal of Automated Reasoning 65: 893–940, 2021.
Publisher's pageAuthors' PDFSupplementary material

Superposition for lambda-free higher-order logic
Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, and Uwe Waldmann. Logical Methods in Computer Science 17(2): 1:1–1:38, 2021.
Publisher's pageAuthors' PDFSupplementary material

Efficient full higher-order unification
Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin. In Ariola, Z.M. (ed.), 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), LIPIcs 167, pp. 5:1–5:17, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2020.
Publisher's pageAuthors' PDFReport (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 11716, pp. 55–73, Springer, 2019.
Publisher's pageAuthors' PDFReport (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.
Publisher's pageAuthors' 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.
Publisher's pageAuthors' PDFReport (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 pageAuthors' PDFSlides (PDF)

An Isabelle formalization of the expressiveness of deep learning (extended abstract)
Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. In Hales, T. C., Kaliszyk, C., Schulz, S., Urban, J. (eds.) 2nd Conference on Artificial Intelligence and Theorem Proving (AITP 2017), pp. 22–23.
Abstract (PDF)Slides (PDF)

Theses:

Superposition for Higher-Order Logic
Alexander Bentkamp. Ph.D. thesis, Vrije Universiteit Amsterdam, 2021.
Ph.D. Thesis (PDF)

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

Homologische Betrachtung des Alexanderpolynoms
Alexander Bentkamp. B.Sc. thesis, Georg-August-Universität Göttingen, 2013.
B.Sc. Thesis (PDF)

Teaching: