On the Power of Temporal Prophecy
recording made private on YouTubehttps://youtu.be/cpzt-5Y1ups
summary
Shows a reduction of liveness/termination to safety in uninterpreted first‑order logic using a fair abstract lasso and a nondeterministic monitor automaton that freezes a finite footprint. Adds temporal prophecy witness constants to the initial footprint so existential choices refine the abstraction. Works under EPR decidability restrictions, implemented in the Ivy-style tooling, and claims to prove termination of the Ackermann function (non‑primitive recursive), so the construction actually succeeds.
AI-written summary · about
related talks
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs
19mSimplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
26mTemporal refinements for Call-By-Push-Value with fixpoint
01h 07mBack to the Future: A Fresh Look at Linear Temporal Logic
41mTotal Functions for Automated Reasoning:Building Terminating Theorem Provers
30mRelatively Complete Verification of Probabilistic Programs
56mOmnisemantics: Smooth Handling of Nondeterminism (Invited talk)
18mDeveloping a Dependently Typed Language with Runtime Proof Search