Alexander Bentkamp

According to our database, Alexander Bentkamp authored at least 22 papers between 2015 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2024

Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory.

Joshua Clune, Yicheng Qian, Alexander Bentkamp, Jeremy Avigad

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

2023

Complete and Efficient Higher-Order Reasoning via Lambda-Superposition.

Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Uwe Waldmann

ACM SIGLOG News, October, 2023

An Impossible Asylum.

Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki

Am. Math. Mon., May, 2023

Superposition for Higher-Order Logic.

Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic

J. Autom. Reason., March, 2023

Mechanical Mathematicians.

Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann

Commun. ACM, 2023

Verified reductions for optimization.

Alexander Bentkamp, Ramon Fernández Mir, Jeremy Avigad

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

HHLPy: Practical Verification of Hybrid Systems Using Hoare Logic.

Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan

Proceedings of the Formal Methods - 25th International Symposium, 2023

2022

Privacy accounting εconomics: Improving differential privacy composition via a posteriori bounds.

Valentin Hartmann, Vincent Bindschaedler, Alexander Bentkamp, Robert West

Proc. Priv. Enhancing Technol., 2022

ARCH-COMP22 Category Report: Hybrid Systems Theorem Proving.

Stefan Mitsch, Bohua Zhan, Huanhuan Sheng, Alexander Bentkamp, Xiangyu Jin, Shuling Wang, Simon Foster, Christian Pardillo Laursen, Jonathan Julián Huerta y Munive

Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22), 2022

2021

The Embedding Path Order for Lambda-Free Higher-Order Terms.

Alexander Bentkamp

FLAP, 2021

Verified Optimization.

Alexander Bentkamp, Jeremy Avigad

CoRR, 2021

Verified Optimization (work in progress).

Alexander Bentkamp, Jeremy Avigad

Proceedings of the Joint Proceedings of the FMM, FVPS, MathUI,NatFoM, and OpenMath Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2021 co-located with the 14th Conference on Intelligent Computer Mathematics (CICM 2021), Virtual Event, Timisoara, Romania, July 26, 2021

Making Higher-Order Superposition Work.

Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret

Proceedings of the Automated Deduction - CADE 28, 2021

Superposition with First-class Booleans and Inprocessing Clausification.

Visa Nummelin, Alexander Bentkamp, Sophie Tourret, Petar Vukmirovic

Proceedings of the Automated Deduction - CADE 28, 2021

Superposition for Full Higher-order Logic.

Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic

Proceedings of the Automated Deduction - CADE 28, 2021

2020

Efficient Full Higher-Order Unification.

Petar Vukmirovic, Alexander Bentkamp, Visa Nummelin

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

2019

Superposition with Lambdas.

Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann

Proceedings of the Automated Deduction - CADE 27, 2019

2018

Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms.

Alexander Bentkamp

Arch. Formal Proofs, 2018

Superposition for Lambda-Free Higher-Order Logic.

Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

A Formal Proof of the Expressiveness of Deep Learning.

Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

2016

Expressiveness of Deep Learning.

Alexander Bentkamp

Arch. Formal Proofs, 2016

2015

Latin Square.

Alexander Bentkamp

Arch. Formal Proofs, 2015