ABSTRACT. Based on our earlier formalization of conflict-driven clause learning (CDCL) in Isabelle/HOL, we refine the CDCL calculus to add a crucial optimization: two watched literals. We formalize the data structure and the invariants. Then we refine the calculus to obtain an executable SAT solver. Through a chain of refinements carried out using the Isabelle Refinement Framework, we target Imperative HOL and extract imperative Standard ML code. Although our solver is not competitive with the state of the art, it offers acceptable performance for some applications, and heuristics can be added to improve it further.

ABSTRACT. This paper presents the tool CodeLazy for Isabelle/HOL. It hooks into Isabelle’s code generator such that the generated code evaluates a user-specified set of type constructors lazily, even in target languages with eager evaluation. The lazy type must be algebraic, i.e., values must be built from constructors and a corresponding case operator decomposes them. Every datatype and codatatype is algebraic and thus eligible for lazification.

Lazification is transparent to the user: definitions, theorems, and the reasoning in HOL need not be changed. Instead, CodeLazy transforms the code equations for functions on lazy types when code is generated. It thus makes code-generation-based Isabelle tools like evaluation and quickcheck available for codatatypes, where eager evaluation frequently causes non-termination. Moreover, as all transformations are checked by Isabelle’s kernel, they cannot introduce correctness problems.

ABSTRACT. The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It thereby approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has several applications in number theory, computer algebra and cryptography.

In a recent paper, we presented the first formal soundness proof of the LLL algorithm. However, this proof did not include a formal statement of its complexity. Therefore, in this paper we provide two formal statements on the polynomial runtime. First, we formally prove a polynomial bound on the number of arithmetic operations. And second, we show that the numbers during the execution stay polynomial in size, so that each arithmetic operation can be performed in polynomial time.

ABSTRACT. Hilbert's tenth problem, posed in 1900 by David Hilbert, asks for a general algorithm to determine the solvability of any given Diophantine equation. In 1970, Yuri Matiyasevich proved the DPRM theorem which implies such an algorithm cannot exist. This paper will outline our attempt to formally state the DPRM theorem and verify Matiyasevich's proof using the proof assistant Isabelle/HOL.

ABSTRACT. Over 32 years, Isabelle has made a long way from a small experimental proof assistant to a versatile platform for proof document development. There has always been a challenge to keep up with the natural growth of applications, notably the Archive of Formal Proofs (AFP). Can we scale this technology further, towards really big libraries of formalized mathematics? Can the underlying Scala/JVM and Poly/ML platforms cope with the demands? Can we eventually do 10 times more and better? In this paper I will revisit these questions particularly from the perspective of: * Editing: Prover IDE infrastructure and front-ends, * Building: batch-mode tools and background services, * Browsing: HTML views and client-server applications.

ABSTRACT. The beginnings of the Isabelle Prover IDE framework (Isabelle/PIDE) go back to the year 2008. This is a report on the project after 10 years, with system descriptions for various PIDE front-ends, namely (1) Isabelle/jEdit, the main PIDE application and default Isabelle user-interface, (2) Isabelle/VSCode, an experimental application of the Language Server Protocol in Visual Studio Code (by Microsoft), and (3) a headless PIDE server with JSON protocol messages over TCP sockets.

ABSTRACT. The System for Automated Deduction (SAD) by Andrei Paskevich proof-checks texts written in nearly natural mathematical language, without explicit system commands or prover commands. Natural language features like soft typing by noun phrases guide efficient text processing and proof checking. We have implemented practical improvements of the checking algorithm and extensions of the input language, so that we are now able to process considerably longer and more complicated texts. These are immediately readable by mathematicians, as demonstrated by subsequent examples. This suggests an approach to formal mathematics through collections or libraries of texts in (a controlled) natural language.

ABSTRACT. We formally prove in Isabelle/HOL two properties of an algorithm for laying out trees visually. The first property states that removing layout annotations recovers the original tree. The second property states that nodes are placed at least a unit of distance apart. We have yet to formalize three additional properties: That parents are centered above their children, that drawings are symmetrical with respect to reflection and that identical subtrees are rendered identically.

ABSTRACT. Substitution under quantifiers is non-trivial and may obscure a proof system for newcomers. Monk (Arch. Math. Log. Grundl. 1965) successfully eliminates substitution via identities and also uses a so-called normalization of formulas as a further simplification. We formalize the substitutionless proof system in Isabelle/HOL, spelling out its side conditions explicitly and verifying its soundness.

ABSTRACT. This is an introduction to the remote_build tool for transparent remote session builds. The intended workflow for a user is to locally issue a build command for some session heap images and then continue working, while the actual build runs on a remote machine and the resulting heap images are synchronized incrementally as soon as they are available.

ABSTRACT. Deciding which sub-tool to use for a given proof state requires expertise specific to each ITP. To mitigate this problem, we present PaMpeR, a proof method recommendation system for Isabelle/HOL. Given a proof state, PaMpeR recommends proof methods to discharge the proof goal and provides qualitative explanations as to why it suggests these methods. PaMpeR generates these recommendations based on existing hand-written proof corpora, thus transferring experienced users' expertise to new users. Our evaluation shows that PaMpeR correctly predicts experienced users' proof methods invocation especially when it comes to special purpose proof methods.

ABSTRACT. We verify functional correctness of insertion sort as well as the partition function of quicksort. We use Isabelle/UTP and its denotational semantics for imperative programs as a verification framework. We propose a forward Hoare VCG for our reasoning and we discuss the different technical challenges encountered while using Isabelle/UTP.