A generic type system with path-sensitive inference and template-based potential functions automatically confirms optimal amortized bounds for skew heaps and leftist heaps.
Title resolution pending
5 Pith papers cite this work. Polarity classification is still indexing.
5
Pith papers citing it
citation-role summary
background 3
citation-polarity summary
verdicts
UNVERDICTED 5roles
background 3polarities
background 3representative citing papers
dARL supplies a sound deductive refinement calculus with trace semantics for verifying and simplifying differential-algebraic programs, shown complete for index reduction certification.
A new orchestral DPLL(T) approach for SMT over prime fields outperforms prior tools on ZKP compiler and circuit benchmarks by balancing completeness and efficiency across coordinated modules.
Encodes arrays as sets of ordered pairs and supplies a decision procedure for a set-theory fragment that lets {log} reason about arrays alongside sets and functions.
ReCent-Prover achieves a 22.58% relative improvement over prior state-of-the-art in proved theorems on the CoqStoq benchmark by using reasoning-centric techniques under a fixed LLM invocation budget.
citing papers explorer
-
Automated Amortised Analysis of Skew Heaps and Leftist Heaps (Extended Version)
A generic type system with path-sensitive inference and template-based potential functions automatically confirms optimal amortized bounds for skew heaps and leftist heaps.
-
A Deductive Refinement Calculus for Differential-Algebraic Programs
dARL supplies a sound deductive refinement calculus with trace semantics for verifying and simplifying differential-algebraic programs, shown complete for index reduction certification.
-
An Effective Orchestral Approach to Satisfiability Modulo Prime Fields
A new orchestral DPLL(T) approach for SMT over prime fields outperforms prior tools on ZKP compiler and circuit benchmarks by balancing completeness and efficiency across coordinated modules.
-
Encoding and Reasoning about Arrays in Constraint Logic Programming with Sets
Encodes arrays as sets of ordered pairs and supplies a decision procedure for a set-theory fragment that lets {log} reason about arrays alongside sets and functions.
-
On Reasoning-Centric LLM-based Automated Theorem Proving
ReCent-Prover achieves a 22.58% relative improvement over prior state-of-the-art in proved theorems on the CoqStoq benchmark by using reasoning-centric techniques under a fixed LLM invocation budget.