ABSTRACT. Verifying existing software is hard: they are developed in languages notamenable to verification, they involve complicated optimizations that obscure the underlying logic, and they are gigantic in size. In this paper, we propose a way to ease this pain via a simplification framework that employs interaction trees as a language-agnostic interface. We show that local variable lifting, the technique underlying AutoCorres for the Simpl language, can be generalized to interaction trees via an implementation in Rocq (formerly Coq). A key challenge with simplifying interaction trees is that they are too dynamic to be pattern-matched on. We address this challenge via metaprogramming. Our metaprogramming framework is semi-automatic and proof-guided, i.e., we obtain the simplified code via a constructive proof of equivalence that can be automated via proof tactics, by utilizing Rocq's Derive extension. This approach gives us simplified code and the equivalence theorem in one step. We demonstrate that our approach is practical using examples inspired by real-world applications.

ABSTRACT. Craig's Interpolation theorem has a wide range of applications, from mathematical logic to computer science. Proof-theoretical techniques for establishing interpolation usually follow a method first introduced by Maehara for the Sequent Calculus and then adapted by Prawitz to Natural Deduction. The result can be strengthened to a proof-relevant version, taking proof terms into account: this was first established by Čubrić in the simply-typed lambda-calculus with sums and more recently extended to linear, classical and intuitionistic sequent calculi. In the present paper, we give a new proof of Čubrić's proof-relevant interpolation theorem by building on principles of bidirectional typing, and formalise it in the Rocq proof assistant.

ABSTRACT. Interactive theorem provers (ITPs) are promising tools for ensuring program correctness, but users often complain about their poor usability and steep learning curve. A common complaint, especially among new users, are confusing error messages that expose details of the ITP's underlying theory or implementation details. In this work, we investigate how adding hints to three types of scope and type checking error messages in the Agda ITP affects the new users' debugging experience. We evaluate the effectiveness and perceived helpfulness of those error messages by conducting a between-subjects user study where we provide a series of Agda code snippets, each containing a single error that the participants have to fix based on the error message. We measure the success rate, time taken to fix the error, and perceived helpfulness for each code snippet with the original as well as the enhanced error message and determine the statistical significance of adding the hint. Our results show that correct hints can improve the success rate and time taken to fix the error, and that error messages with hints are rated significantly more helpful than those without. Additionally, we find that while error messages with incorrect hints are often rated as more misleading, they do not significantly impact the success rate or time taken to fix the error. These results show that adding hints to error messages is a viable step on the path towards making ITPs more widely accessible.

ABSTRACT. Intermediate Verification Languages (IVLs) play the same role in verification as Intermediate Representations in compilation, a layer that separates a verifier's language-specific front-end from its logic automation back-end. Successful IVL tools such as Boogie, Why3, and Viper generate Verification Conditions (VCs) that are sent to an SMT solver. The verifier output can be trusted only if these VCs are sound with respect to the formal semantics of the IVL. Formalizing the semantics of IVLs and verifying the soundness of corresponding VC Generators with respect to this semantics is challenging if one wants to model realistic features of IVLs such as mutually recursive definitions, lexical variable and contol-flow labeled scopes, interpreted and uninterpreted functions, and unbounded loops. B3 is a new IVL. This paper presents a formalization of B3's semantics, a VC Generator for the language, and a soundness proof that these two correspond. All three components are authored in the Dafny programming language and verifier. The key theoretical contribution of this work is a methodology to split the IVL's semantic encodings into two layers of abstraction to cover realistic aspects of the semantics, while keeping the proofs amenable to automation. Optimized for Dafny-style automation, the first layer is used to verify the soundness of the VC Generator procedure. Optimized for expressiveness, the second layer is used to capture the semantics in a natural way.

ABSTRACT. We benchmark four proof assistants (Agda, Idris 2, \lean and \rocq) through a single test suite. We focus our benchmarks on the basic features that all systems based on a similar foundations (dependent type theory) have in common. We do this by creating an ``over language'' in which to express all the information we need to be able to output correct and idiomatic syntax for each of our targets. Our benchmarks further focus on ``basic engineering'' of these systems: how do they handle long identifiers, long lines, large records, large data declarations, and so on. Our benchmarks reveals both flaws and successes in all systems. We give a thorough analysis of the results. We also detail the design of our extensible system. It is designed so that additional tests and additional system versions can easily be added. A side effect of this work is a better understanding of the common abstract syntactic structures of all four systems.

ABSTRACT. This paper introduces the algebra normalizing tactic for the Lean theorem prover. This tactic expands on the existing ring tactic by additionally supporting a scalar multiplication action over a fixed commutative (semi)ring. It supports rational constants in the base ring even when the main ring is not a field, which lets us implement a suite of tactics for manipulating both univariate and multivariate polynomials. These features are implemented by adapting the existing implementation of ring while retaining support for variable exponents.

ABSTRACT. Vampire proves theorems completely automatically in first- and higher-order logic extended with theories. Proof checking is increasingly demanded to consolidate user trust in Vampire's output. We describe ongoing efforts in reconstructing Vampire proofs as trusted proofs in Lean.

ABSTRACT. The free-variable tableau method has been widely used in order to automate proofs in multiple kinds of logics. Many Automated Theorem Provers (ATPs) rely on this approach, either because it is the only available method (e.g., in certain modal logics) or because it facilitates the generation of proof certificates. However, as far as the authors know, its results have never been formalized in a proof assistant. In this paper, we present TableauxRocq, a deep-embedding of free-variable first-order tableaux in the Rocq prover. The formalized calculus is proved sound and provides a modular Skolemization system that enables the use of Skolemization-based optimisations. Moreover, we show how TableauxRocq can be used as a certifier for ATPs by adapting the Goeland prover to output proofs in the TableauxRocq format. By using the full power of reflection, thereby providing a fully certified proof checker for free, we show that the deep embedding performs at least as well as a shallow embedding, even without proof optimizations, and strictly better when Skolemization-related optimizations are present in the proof.

ABSTRACT. Real root isolation is a fundamental subroutine in computer algebra, with applications ranging from algebraic number arithmetic to solving polynomial systems. Modern implementations typically employ subdivision methods based on root counting via Descartes’ rule of signs. In contrast, most existing formally verified root isolation procedures rely on Sturm’s theorem for root counting, leading to a noticeable gap between practical implementations and formally verified approaches. We take an initial step toward efficient verified real root isolation by formally verifying two simple algorithms based on Descartes’ rule of signs: a classical bisection procedure and a Newton-accelerated variant. In this paper, we describe the algorithms and present formal proofs of termination, soundness, and completeness. Brief experiments show promising performance improvements over existing formally verified approaches in Isabelle/HOL.