5 papers
A Cost-Aware Probability Monad for Liquid Haskell
Matthias Hetzenberger, Georg Moser, Florian Zuleger
Probabilistic algorithms and data structures are widely used to obtain favourable expected performance guarantees. While their mathematical analysis is often well understood, mecha…
Term Orders for Optimistic Lambda-Superposition
Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger
We introduce KBO and LPO, two variants of the Knuth-Bendix order (KBO) and the lexicographic path order (LPO) designed for use with the -superposition calculus. We esta…
Optimistic Higher-Order Superposition
Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger +1
The -superposition calculus is a successful approach to proving higher-order formulas. However, some parts of the calculus are extremely explosive, notably due to the higher-or…
The Vampire Diary
Filip Bártek, Ahmed Bhayat, Robin Coutelier +10
During the past decade of continuous development, the theorem prover Vampire has become an automated solver for the combined theories of commonly-used data structures. Vampire now…
To Zip Through the Cost Analysis of Probabilistic Programs
Matthias Hetzenberger, Georg Moser, Florian Zuleger
Probabilistic programming and the formal analysis of probabilistic algorithms are active areas of research, driven by the widespread use of randomness to improve performance. While…