Higher-order Automation In TLAPS
summary
Implements a direct THF export from TLA+ and adds Zipperposition as a higher-order backend, so TLAPS no longer needs heavy eliminations for operator-parameterized lemmas. The prototype proves the recursive sum examples reliably by higher-order search, but currently lacks integration with arithmetic/SMT reasoning and runs slower than tuned first-order encodings. Future work targets performance parity, a larger benchmark run, and a sets-as-predicates encoding to reduce ad hoc axioms.
AI-written summary · about
chapters (8)
- 0:00Intro
- 0:14Summary
- 1:06TLAPS in a Nutshell
- 2:09Defining the Sum Operator in TLA+
- 4:07Proving Basic Properties
- 7:11Second-order Logic in TLA+
- 9:52Experiments with Zipperposition
- 11:34Perspectives
related talks
18mA Verified Compiler for a Functional Tensor Language
01h 07mBack to the Future: A Fresh Look at Linear Temporal Logic
45mLogic Meta Programming for Functional Languages
29mHigher-Order Weakest Precondition Transformers via a CPS Transformation
24mVerified Tensor-Program Optimization Via High-Level Scheduling Rewrites
28mSynthesizing Abstract Transformers
29mSynthesizing Axiomatizations using Logic Learning
31mDependent tagless final