Related papers: Formalising Sylow's theorems in Coq

This report presents a formalization of May's theorem in the proof assistant Coq. It describes how the theorem statement is first translated into Coq definitions, and how it is subsequently proved. Various aspects of the proof and related…

We present a first step towards the Coq implementation of the Theory of Tagged Objects formalism. The concept of tagged types is encoded, and the soundness proofs are discussed with some future work suggestions.

We present a Coq formalization of the Quantified Reflection Calculus with one modality, or $\mathsf{QRC}_1$. This is a decidable, strictly positive, and quantified modal logic previously studied for its applications in proof theory. The…

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…

In this paper we formalize some foundation concepts and theorems of group theory in a variant of type theory called the Calculus of Constructions with Definitions. In this theory we introduce definition of a group, which is both general and…

Theory of choreographic languages typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of them lead to long reviewing processes, and occasionally to…

We show a classification method for finite groupoids and discuss the cardinality of cosets and its relation with the index. We prove a generalization of the Lagrange's Theorem and establish a Sylow theory for groupoids.

This notes explains how standard algorithms that construct sorting networks have been formalised and proved correct in the Coq proof assistant using the SSReflect extension.

We describe a formalization of higher-order rewriting theory and formally prove that an AFS is strongly normalizing if it can be interpreted in a well-founded domain. To do so, we use Coq, which is a proof assistant based on dependent type…

Matching logic is a formalism for specifying, and reasoning about, mathematical structures, using patterns and pattern matching. Growing in popularity, it has been used to define many logical systems such as separation logic with recursive…

Formalization of real analysis offers a chance to rebuild traditional proofs of important theorems as unambiguous theories that can be interactively explored. This paper provides a comprehensive overview of the Lebesgue Differentiation…

For performance and verification in machine learning, new methods have recently been proposed that optimise learning systems to satisfy formally expressed logical properties. Among these methods, differentiable logics (DLs) are used to…

Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised implementations can be generated automatically. Theory of…

We describe a project to formalize Galois theory using the Lean theorem prover, which is part of a larger effort to formalize all of the standard undergraduate mathematics curriculum in Lean. We discuss some of the challenges we faced and…

This paper describes a formalization of discrete real closed fields in the Coq proof assistant. This abstract structure captures for instance the theory of real algebraic numbers, a decidable subset of real numbers with good algorithmic…

The theorem of three circles in real algebraic geometry guarantees the termination and correctness of an algorithm of isolating real roots of a univariate polynomial. The main idea of its proof is to consider polynomials whose roots belong…

We make explicit certain results around the Galois correspondence in the context of definable automorphism groups, and point out the relation to some recent papers dealing with the Galois theory of algebraic differential equations when the…

This is the third and final installment of an exposition of an ACL2 formalization of finite group theory. Part I covers groups and subgroups, cosets, normal subgroups, and quotient groups. Part II extends the theory in the developmnent of…

We investigate which aspects of recent developments on Galois corings and comodules admit a formulation in terms of comonads. This approach hopefully will permit of focusing in what is specific in each particular future situation, having…

Initial Semantics aims at characterizing the syntax associated to a signature as the initial object of some category. We present an initial semantics result for typed higher-order syntax together with its formalization in the Coq proof…