Alexander Bentkamp

Drafts:

Complete and efficient higher-order reasoning via lambda-superposition
Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, and Uwe Waldmann.
Draft (PDF)

Publications:

Finding mathematical proofs using computers
Alexander Bentkamp, Jasmin Blanchette.
Nieuw Archief voor Wiskunde 5/24(2): 114–118, 2023
Publisher's PDF ⋅ Preprint (PDF)

Verified Reductions for Optimization
Alexander Bentkamp, Ramon Fernández Mir, Jeremy Avigad.
In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), LNCS, Springer.
Publisher's page ⋅ Preprint (PDF)

HHLPy: Practical Verification of Hybrid Systems using Hoare Logic
Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan.
In: Chechik, M., Katoen, JP., Leucker, M. (eds.) Formal Methods (FM 2023), LNCS, Springer.
Publisher's page ⋅ Preprint (PDF)

Superposition for Higher-Order Logic
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirović. Journal of Automated Reasoning 67: Article number: 10, 2023.
Publisher's page ⋅ Preprint (PDF) ⋅ Errata (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 page ⋅ Preprint (PDF)

An Impossible Asylum
Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, and Wojciech Nawrocki.
The American Mathematical Monthly, 130:5, 446-453
Publisher's page ⋅ Preprint (PDF)

Mechanical Mathematicians
Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann.
Communications of the ACM 66(4): 80–90, 2023
Preprint (PDF)

Verified Optimization (work in progress)
Alexander Bentkamp and Jeremy Avigad.
In Blanchette, J., Naumowicz, A. (eds.) Fifth Workshop on Formal Mathematics for Mathematicians (FMM 2021), CEUR Workshop Proceedings (CEUR-WS.org).
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 page ⋅ Authors' PDF

The Embedding Path Order for Lambda-Free Higher-Order Terms
Alexander Bentkamp. Journal of Applied Logics 8(10): 2447-2469, 2021.
Publisher's page ⋅ Authors' PDF ⋅ Supplementary material ⋅ Slides (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 page ⋅ Authors' PDF ⋅ Report (PDF) ⋅ Slides (PDF) ⋅ Errata (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 page ⋅ Authors' PDF ⋅ Report (PDF) ⋅ Errata (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 page ⋅ Authors' 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 page ⋅ Authors' PDF ⋅ Supplementary 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 page ⋅ Authors' PDF ⋅ Supplementary 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 page ⋅ Authors' PDF ⋅ 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 11716, pp. 55–73, Springer, 2019.
Publisher's page ⋅ Authors' 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.
Publisher's page ⋅ Authors' 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 page ⋅ Authors' 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 ⋅ Authors' PDF ⋅ Slides (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.
PhD Thesis (PDF) ⋅ Errata (PDF)

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

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

Teaching:

• Computergestützte Beweisführung 2023/24
• Mathematik für Wirtschaftswissenschaftler II (Exercises) 2023
• Logical Verification 2019/20
• Logical Verification 2018/19 (Teaching assistant)
• Advanced Logic 2017/18 (Teaching assistant)