Alexander Bentkamp

36 papers A 5B 4Journal 24Unranked 3
YearRankTypeTitle / Venue / Authors
2025 J jnl
Optimistic Higher-Order Superposition.
CoRR
Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger, Uwe Waldmann
2025 J jnl
Term Orders for Optimistic Lambda-Superposition.
CoRR
Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger
2024 B conf
Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory.
ITP
Joshua Clune, Yicheng Qian, Alexander Bentkamp, Jeremy Avigad
2023 J jnl
An Impossible Asylum.
Am. Math. Mon.
Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki
2023 J jnl
Complete and Efficient Higher-Order Reasoning via Lambda-Superposition.
ACM SIGLOG News
Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Uwe Waldmann
2023 B conf
HHLPy: Practical Verification of Hybrid Systems Using Hoare Logic.
FM
Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan
2023 J jnl
Mechanical Mathematicians.
Commun. ACM
Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann
2023 J jnl
Superposition for Higher-Order Logic.
J. Autom. Reason.
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic
2023 — conf
Verified reductions for optimization.
TACAS (2)
Alexander Bentkamp, Ramon Fernández Mir, Jeremy Avigad
2023 J jnl
Verified reductions for optimization.
CoRR
Alexander Bentkamp, Ramon Fernández Mir, Jeremy Avigad
2022 — conf
ARCH-COMP22 Category Report: Hybrid Systems Theorem Proving.
ARCH@SAFECOMP
Stefan Mitsch, Bohua Zhan, Huanhuan Sheng, Alexander Bentkamp, Xiangyu Jin, Shuling Wang, Simon Foster, Christian Pardillo Laursen, Jonathan Julián Huerta y Munive
2022 J jnl
HHLPy: Practical Verification of Hybrid Systems using Hoare Logic.
CoRR
Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan
2022 J jnl
Making Higher-Order Superposition Work.
J. Autom. Reason.
Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret
2022 J jnl
Privacy accounting εconomics: Improving differential privacy composition via a posteriori bounds.
CoRR
Valentin Hartmann, Vincent Bindschaedler, Alexander Bentkamp, Robert West
2022 J jnl
Privacy accounting εconomics: Improving differential privacy composition via a posteriori bounds.
Proc. Priv. Enhancing Technol.
Valentin Hartmann, Vincent Bindschaedler, Alexander Bentkamp, Robert West
2021 J jnl
An Impossible Asylum.
CoRR
Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki
2021 J jnl
Efficient Full Higher-Order Unification.
Log. Methods Comput. Sci.
Petar Vukmirovic, Alexander Bentkamp, Visa Nummelin
2021 A conf
Making Higher-Order Superposition Work.
CADE
Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret
2021 A conf
Superposition for Full Higher-order Logic.
CADE
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic
2021 J jnl
Superposition for Lambda-Free Higher-Order Logic.
Log. Methods Comput. Sci.
Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann
2021 A conf
Superposition with First-class Booleans and Inprocessing Clausification.
CADE
Visa Nummelin, Alexander Bentkamp, Sophie Tourret, Petar Vukmirovic
2021 J jnl
Superposition with Lambdas.
CoRR
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann
2021 J jnl
Superposition with Lambdas.
J. Autom. Reason.
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann
2021 J jnl
The Embedding Path Order for Lambda-Free Higher-Order Terms.
FLAP
Alexander Bentkamp
2021 — conf
Verified Optimization (work in progress).
CICM Workshops
Alexander Bentkamp, Jeremy Avigad
2021 J jnl
Verified Optimization.
CoRR
Alexander Bentkamp, Jeremy Avigad
2020 B conf
Efficient Full Higher-Order Unification.
FSCD
Petar Vukmirovic, Alexander Bentkamp, Visa Nummelin
2020 J jnl
Efficient Full Higher-Order Unification.
CoRR
Petar Vukmirovic, Alexander Bentkamp, Visa Nummelin
2020 J jnl
Superposition for Lambda-Free Higher-Order Logic.
CoRR
Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann
2019 J jnl
A Formal Proof of the Expressiveness of Deep Learning.
J. Autom. Reason.
Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow
2019 A conf
Superposition with Lambdas.
CADE
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann
2018 J jnl
Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms.
Arch. Formal Proofs
Alexander Bentkamp
2018 A conf
Superposition for Lambda-Free Higher-Order Logic.
IJCAR
Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann
2017 B conf
A Formal Proof of the Expressiveness of Deep Learning.
ITP
Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow
2016 J jnl
Expressiveness of Deep Learning.
Arch. Formal Proofs
Alexander Bentkamp
2015 J jnl
Latin Square.
Arch. Formal Proofs
Alexander Bentkamp