Related papers: A Formalisation of Algorithms for Sorting Network

Termination is an important property of programs; notably required for programs formulated in proof assistants. It is a very active subject of research in the Turing-complete formalism of term rewriting systems, where many methods and tools…

In this project, a rather complete proof-theoretical formalization of Lambek Calculus (non-associative with arbitrary extensions) has been ported from Coq proof assistent to HOL4 theorem prover, with some improvements and new theorems.…

Verification of neural networks relies on activation functions being piecewise affine (pwa) -- enabling an encoding of the verification problem for theorem provers. In this paper, we present the first formalization of pwa activation…

In a small-step semantics with a deterministic reduction strategy, refocusing is a transformation that connects a reduction-based normalization function (i.e., a normalization function that enumerates the successive terms in a reduction…

Due to their numerous advantages, formal proofs and proof assistants, such as Coq, are becoming increasingly popular. However, one disadvantage of using proof assistants is that the resulting proofs can sometimes be hard to read and…

A theory is developed which uses "networks" (directed acyclic graphs with some extra structure) as a formalism for expressions in multilinear algebra. It is shown that this formalism is valid for arbitrary PROPs (short for 'PROducts and…

Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from graph theory that was carried out in three proof assistants:…

Computer Algebra systems are widely spread because of some of their remarkable features such as their ease of use and performance. Nonetheless, this focus on performance sometimes leads to unwanted consequences: algorithms and computations…

We introduce a generalization of the conventional renormalization schemes used in dimensional regularization, which illuminates the renormalization scheme and scale ambiguities of pQCD predictions, exposes the general pattern of…

In this paper we give a preliminary formalization of the p-adic numbers, in the context of the second author's univalent foundations program. We also provide the corresponding code verifying the construction in the proof assistant Coq.…

We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of…

We give a brief discussion of some of the issues which have arisen in the course of formalizing some classical set-theoretical mathematics in the Coq system. This sprouts from, expands and replaces a chapter of math.HO/0311260 which will be…

We introduce Refinement Reflection, a new framework for building SMT-based deductive verifiers. The key idea is to reflect the code implementing a user-defined function into the function's (output) refinement type. As a consequence, at uses…

Largely adopted by proof assistants, the conventional induction methods based on explicit induction schemas are non-reductive and local, at schema level. On the other hand, the implicit induction methods used by automated theorem provers…

We consider regularized support vector machines (SVMs) and show that they are precisely equivalent to a new robust optimization formulation. We show that this equivalence of robust optimization and regularization has implications for both…

We present an approach for representing abstract argumentation frameworks based on an encoding into classical higher-order logic. This provides a uniform framework for computer-assisted assessment of abstract argumentation frameworks using…

We present three projects concerned with applications of proof assistants in the area of programming language theory and mathematics. The first project is about a certified compilation technique for a domain-specific programming language…

We give a method to transform into programs, classical proofs using a well ordering of the reals. The technics uses a generalization of Cohen's forcing and the theory of classical realizability introduced by the author.

The motivation for this paper comes out of our experience with teaching natural deduction (ND) and with the way this formal system is implemented by the \textsc{Coq} proof assistant, namely by means of so-called tactics, which are…

We present formalized proofs verifying that the first-order unification algorithm defined over lists of satisfiable constraints generates a most general unifier (MGU), which also happens to be idempotent. All of our proofs have been…