ABSTRACT. A consistent thread running through the three decades of Voevodsky's work is
the application of the ideas of homotopy theory in new and surprising ways,
first to motives, and then to formalization of proofs and the foundations of
mathematics.  I will present the story of the latter development, focusing on
the points of interest to mathematicians.

ABSTRACT. For calculational proofs as they are propagated by Gries and Schneider's textbook classic “A Logical Approach to Discrete Math” (LADM), automated proof checking is feasible, and can provide useful feedback to students acquiring and practicing basic proof skills. We report on the CalcCheck system which implements a proof checker for a mathematical language that resembles the rigorous but informal mathematical style of LADM so closely that students very quickly recognise the system as not an obstacle, but as an aid, and realise that the problem is finding proofs.

Students interact with this trough the “web application” front-end CalcCheckWeb which provides some assistance for proof entry, but intentionally no assistance for proof finding. Upon request, the system displays, side-by-side with the student input, a version of that annotated with the results of checking each step for correctness.

CalcCheckWeb has now been used twice for teaching this course, and students have been solving exercises and submitting assignments, midterms, and final exams on the system ─ for examinations, there is the option to disable proof checking and leave only syntax checking enabled. CalcCheck also performed the grading, with very limited human overriding necessary.

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 this paper, we develop the first mechanized soundness proof of the LLL algorithm using Isabelle/HOL. We additionally integrate one application of LLL, namely a verified factorization algorithm for integer polynomials which runs in polynomial time.

ABSTRACT. In this work we are interested in minimal complete sets of solutions for homogeneous linear diophantine equations. Such equations naturally arise during AC-unification, that is, unification in the presence of associative and commutative symbols. Minimal complete sets of solutions are required to compute AC-critical pairs. We present a verified solver for homogeneous linear diophantine equations that we formalized in Isabelle/HOL. Our work provides the basis for formalizing AC-unification and will eventually enable the certification of automated AC-confluence and AC-completion tools.

ABSTRACT. Coq provides linear arithmetic tactics such as omega or lia. Currently, these tactics either fully prove the current goal in progress, or fail. We propose to improve this behavior: when the goal is not provable in linear arithmetic, we inject in hypotheses new equalities discovered from the linear inequalities. These equalities may help other Coq tactics to discharge the goal. In other words, we apply -- in interactive proofs -- one of the seminal idea of SMT-solving: combining tactics by exchanging equalities.

The paper describes how we have implemented equality learning in a new Coq tactic, dealing with linear arithmetic over rationals. It also illustrates how this tactic interacts with other Coq tactics.

ABSTRACT. The use of Hoare logic in combination with weakest preconditions and strongest postconditions is a standard tool for program verification, known as backward and forward reasoning. In this paper we extend these techniques to allow backward and forward reasoning for separation logic. While the former is derived directly from the standard operators of separation logic, the latter uses a new operator. We implement our framework in the interactive theorem prover Isabelle/HOL, and enable automation with several interactive proof tactics.

ABSTRACT. We present a new strategy for performing reification in Coq. That is, we show how to generate first-class abstract syntax trees from ``native'' terms of Coq's logic, suitable as inputs to verified proof procedures in the *proof by reflection* style. Our new strategy, based on the pattern tactic, is simple, short, and fast. We survey the existing methods of reification, describing various design choices and tricks that can be used to speed them up, as well as various limitations. Our strategy is not a good fit, for example, when a term must be reified without performing βιζ reduction. We describe the results of benchmarking 18 variants of reification, in addition to our own, finding that our own reification outperforms 16 of these methods in all cases, and one additional method in some cases; the fastest method of reification we tested is writing an OCaml plugin. Our method is the most concise of the strategies we considered, requiring only two to four lines of Ltac---beyond lists of the identifiers to reify and their reified variants---to reify a term. Additionally, our strategy automatically provides error messages which are no less helpful than Coq's own error messages.

ABSTRACT. In this article, we use the Coq proof assistant to specify and verify the low level layer of SQL’s execution engines. To reach our goals, we first design a high level Coq specification for data and data-centric operators intended to capture their essence. We, then, provide two Coq implementations of our specification. The first one, the physical algebra, consists in the low level operators found in systems such as Postgresql or Oracle. The second, SQL algebra, is an extended relational algebra that provides a semantics for SQL. Last, we formally relate physical algebra and SQL algebra. By proving that the physical algebra implements SQL algebra, we give high level assurances that physical algebraic and SQL algebra expressions enjoy the same semantics. All this yields the first, to our best knowledge, formalisation in Coq of the low level primitives that constitute the main part of SQL execution engines.

ABSTRACT. In this paper we describe an Agda-based formalization of results from Uresin and Dubois' ``Parallel Asynchronous Algorithms for Discrete Data.'' That paper investigates a large class of iterative algorithms that can be transformed into asynchronous processes. In their model each node asynchronously performs partial computations and communicates results to other nodes using unreliable channels.  Uresin and Dubois provide sufficient conditions on iterative algorithms that guarantee convergence to unique fixed points for the associated asynchronous iterations. Proving such sufficient conditions for an iterative algorithm is often dramatically simpler than reasoning directly about an asynchronous implementation. These results are used extensively in the literature of distributed computation, making formal verification worthwhile.

Our Agda library provides users with a collection of sufficient conditions, some of which mildly relax assumptions made in the original paper. Our primary application has been in reasoning about the correctness of network routing protocols. To do so we have derived a new sufficient condition based on the ultrametric theory of Alexander Gurney. This was needed to model the complex policy-rich routing protocol that maintains global connectivity in the internet. 

ABSTRACT. Template-Coq is a plugin for Coq, originally implemented by Malecha, which provides a reifier for Coq terms and global declarations, as represented in the Coq kernel, as well as a denotation command. Initially, it was developed for the purpose of writing functions on Coq’s AST in Gallina. Recently, it was used in the CertiCoq certified compiler project, as its front-end language, to derive parametricity properties, and to extract Coq terms to a CBV λ-calculus. However, the syntax lacked semantics, be it typing semantics or operational semantics, which should reflect, as formal specifications in Coq, the semantics of Coq’s type theory itself. The tool was also rather bare bones, providing only rudimentary quoting and unquoting commands. We generalize it to handle the entire Calculus of Inductive Constructions, as implemented by Coq, including the kernel’s declaration structures for definitions and inductives, and implement a monad for general manipulation of Coq’s logical environment. We demonstrate how this setup allows the definition of many kinds of general purpose plugins, whose correctness can be readily proved in the system itself, and that can be run efficiently after extraction. We give a few examples of implemented plugins, including a parametricity translation. We also advocate the use of Template-Coq as a foundation for higher-level tools.

ABSTRACT. Logic and probability are ancient subjects whose unification holds significant potential for the field of artificial intelligence. The BLOG (Bayesian LOGic) language provides a way to write probability models using syntactic and semantic devices from first-order logic. In modern parlance, it is a relational, open-universe probabilistic programming language that allows one to define probability distributions over the entire space of first-order model structures that can be constructed given the constant, function, and predicate symbols of the program. In this public lecture, Stuart Russell will describe the language mainly through examples and cover its application to monitoring the Comprehensive Nuclear-Test-Ban Treaty.