354 papers · page 5 of 18
In differential topology and geometry, the h-principle is a property enjoyed by certain construction problems. Roughly speaking, it states that the only obstructions to the existence of a solution come from algebraic topology. We describe a formalisation in Lean of the local h-p…
Proofs automatically generated by interactive or automated theorem provers are often several orders of magnitude larger than proofs written by hand. This implies significant challenges for processing such proofs efficiently. It turns out that the data structures used to encode te…
A surprising result of Pitts (1992) says that propositional quantifiers are definable internally in intuitionistic propositional logic (IPC). The main contribution of this paper is to provide a formalization of Pitts’ result in the Coq proof assistant, and thus a verified impleme…
In this paper we describe the design and implementation of feqb, a tool that synthesizes sound equality tests for inductive data types in the dependent type theory of the Coq system. Our procedure scales to large inductive data types, as in hundreds of constructors, since the ter…
The Gated Static Single Assignment (GSA) form was proposed by Ottenstein et al. in 1990, as an intermediate representation for implementing advanced static analyses and optimisation passes in compilers. Compared to SSA, GSA records additional data dependencies and provides more c…
Machine learning techniques have been included in various theorem proving tools for approximately two decades. Some of the learning tasks are well understood and tools actually help practitioners, while other tasks are still in their early developmental stages. In this talk I wil…
Several critical pair criteria are known that guarantee confluence of left-linear term rewrite systems. The correctness of most of these have been formalized in a proof assistant. An important exception has been the development closedness criterion of van Oostrom. Its proof requi…
We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the first-order logic of real arithmetic to a logically equivalent quantifier-free formula. The …
We describe our formalisation in the interactive theorem prover Isabelle/HOL of the Balog–Szemerédi–Gowers Theorem, a profound result in additive combinatorics which played a central role in Gowers’s proof deriving the first effective bounds for Szemerédi’s Theorem. The proof is …
In Homotopy Type Theory, cohomology theories are studied synthetically using higher inductive types and univalence. This paper extends previous developments by providing the first fully mechanized definition of cohomology rings. These rings may be defined as direct sums of cohomo…
We present Aesop, a proof search tactic for the Lean 4 interactive theorem prover. Aesop performs a tree-based search over a user-specified set of proof rules. It supports safe and unsafe rules and uses a best-first search strategy with customisable prioritisation. Aesop also all…
Sharkovsky's theorem is a celebrated result by Ukrainian mathematician Oleksandr Sharkovsky in the theory of discrete dynamical systems, including the fact that if a continuous function of reals has a point of period 3, it must have points of any period. We formalise the proof in…
Abstract Syntax Notation One (ASN.1) is a language for structured data exchange between computers, standardized by both ITU-T and ISO/IEC since 1984. The Distinguished Encoding Rules (DER) specify its non-malleable binary format: for a given ASN.1 data type, every value has a dis…
The number of attacks and accidents leading to significant losses of crypto-assets is growing. According to Chainalysis, in 2021, approx. $14 billion has been lost due to various incidents, and this number is dominated by Decentralized Finance (DeFi) applications. To address thes…
P4Cub is a new intermediate representation (IR) for the P4 programming language. It has been designed with the goal of facilitating development of certified tools. To achieve this, P4Cub is organized around a small set of core constructs and avoids side effects in expressions, wh…
Our objective is to formally verify the correctness of the hundreds of expression optimization rules used within the GraalVM compiler. When defining the semantics of a programming language, expressions naturally form abstract syntax trees, or, terms. However, in order to facilita…
We present the formalization of Doob’s martingale convergence theorems in the mathlib library for the Lean theorem prover. These theorems give conditions under which (sub)martingales converge, almost everywhere or in L1. In order to formalize those results, we build a definition …
In previous work ("From signatures to monads in UniMath"),we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library based on the Coq proof assistant. In the present work, we describe what was necessary to generalize tha…
Skeletal semantics is a framework to describe semantics of programming languages. We propose an automatic generation of a certified OCaml interpreter for any language written in skeletal semantics. To this end, we introduce two new interpretations, i.e., formal meanings, of skele…
The formal verification of the seL4 microkernel started as a research project in 2004 and has achieved commercial scale now, in the number of properties proven, the supported features and platforms, the adoption and deployment by industry and government organisations. It is suppo…