Certified Infinite Descent Criteria in Isabelle/HOL

QuickChecking Convergence of Rewriting Systems (Functional Pearl)

A QuickCheck testing method based on generating and shrinking random execution traces based on checking if the first and last terms of a generated trace share the same deterministic normal form that efficiently finds counterexamples and enables fast, robust shrinking.

Compositional Generator Equivalence

This paper provides a formal account of the syntax and semantics of Hedgehog, a popular PBT framework, and proves that Hedgehog→ possesses a compositional distribution semantics, and introduces Hedgehog→, a restricted version of the language based on the arrow calculus, and proves that Hedgehog→ possesses a compositional distribution semantics.

Descriptive Complexity in Lean: Completeness by First-Order Reductions

We show that descriptive complexity can serve as a foundation for formalizing computational complexity results in a proof assistant, by constructing a Lean library centered around the following concepts: decision problems are isomorphism-invariant predicates on finite structures; complexity classes are defined by their logical characterization; membership is shown by definability witnesses; hardness is shown by first-order reductions from a known hard problem. We also establish bridges to traditional machine models such as (non)deterministic Turing machines. The library proves 73 completeness results, on 68 problems or problem families, over 14 different classes; relations between the classes established inside the logic and not by machine simulation, among them NL = coNL and the Abiteboul-Vianu theorem; and unconditional lower bounds, among them $\mathrm{FO}(\leq) \subsetneq \mathrm{FO}(\leq, \mathrm{TC})$ and the failure of order-free FO(IFP) to capture PTIME.

Guarded Realization Semantics: Occurrence-Sensitive Certificates and Behavior-Dependent Lower Bounds

Distinct proofs, programs, formulas, or rewrite paths may have the same observable behavior while differing in occurrence structure, sharing, interfaces, or transformation history. We develop a guarded realization semantics that retains these distinctions when an error is extracted. The resulting error magnitude is bounded above by a certificate attached to the chosen realization and below by the greatest lower bound determined solely by the observed behavior. For linear double-pushout rewriting in a typed presheaf setting, we identify the greatest subobject transported intact through a rewrite step and through a finite rewrite path. Guarded local estimates compose to give pathwise upper certificates. At the set level, the complementary lower bound is the infimum of magnitudes in a behavior fiber. For non-discrete categories, it is given by a pointwise right Kan extension when that extension exists, and it reduces to the strict-fiber infimum under a Grothendieck fibration hypothesis. For continuous surjective linear observations onto finite-dimensional normed spaces, the lower reflection is the induced quotient norm. Applied to finitely many distinct characters on a compact metrizable abelian group, this yields an interpolation norm with an exact dual formula. Continuous and discrete Abel transfer theorems then convert observed coefficients into lower bounds for tail amplitudes, with consequences for Mellin transforms, generating functions, and normalized point-count errors of curves over finite fields. Under the stated guards and soundness hypotheses, every realization satisfies $Q(O(\mathrm{Err}(r))) \leq A(\mathrm{Err}(r)) \leq U(r)$.

Crimps: Indexical Separation Logics for Order-Invariant Specifications

Towards a Deductive Verification Infrastructure for Weighted Programming

This work presents a deductive verification framework based on a weighted assertion language and an intermediate verification language, whose weight domains are ordered structures with implication and coimplication, which let verification conditions express lower- and upper-bound obligations internally.