Related papers: Initial Semantics for higher-order typed syntax in…

An efficient intuitionistic first-order prover integrated into Coq is useful to replay proofs found by external automated theorem provers. We propose a two-phase approach: An intuitionistic prover generates a certificate based on the matrix…

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…

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…

The key to the proof-theoretic study of a logic is a proof calculus with a subformula property. Many different proof formalisms have been introduced (e.g. sequent, nested sequent, labelled sequent formalisms) in order to provide such…

We present the formalization of a theory of syntax with bindings that has been developed and refined over the last decade to support several large formalization efforts. Terms are defined for an arbitrary number of constructors of varying…

We present the first definition of strictly associative and unital $\infty$-category. Our proposal takes the form of a type theory whose terms describe the operations of such structures, and whose definitional equality relation enforces…

In this paper we provide a semantic and syntactic analysis of parametrised natural numbers object in coherent categories, or pr-coherent categories. Semantically, we show the definable functions in the initial pr-coherent category are…

Sharing of notations and theories across an inheritance hierarchy of mathematical structures, e.g., groups and rings, is important for productivity when formalizing mathematics in proof assistants. The packed classes methodology is a…

In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical…

CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive…

There are multiple ways to formalise the metatheory of type theory. For some purposes, it is enough to consider specific models of a type theory, but sometimes it is necessary to refer to the syntax, for example in proofs of canonicity and…

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…

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 syntax of an imperative language does not mention explicitly the state, while its denotational semantics has to mention it. In this paper we present a framework for the verification in Coq of properties of programs manipulating the…

Traditional category theory is typically based on set-theoretic principles and ideas, which are often non-constructive. An alternative approach to formalizing category theory is to use E-category theory, where hom sets become setoids. Our…

One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful programs is desirable, it is not yet mainstream. This is partly…

Compiler correctness proofs for higher-order concurrent languages are difficult: they involve establishing a termination-preserving refinement between a concurrent high-level source language and an implementation that uses low-level shared…

Dependent Object Types (DOT) is intended to be a core calculus for modelling Scala. Its distinguishing feature is abstract type members, fields in objects that hold types rather than values. Proving soundness of DOT has been surprisingly…

Classical first-order logic is in many ways central to work in mathematics, linguistics, computer science and artificial intelligence, so it is worthwhile to define it in full detail. We present soundness and completeness proofs of a…

Context-free grammar simplification is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formalization, using the Coq proof assistant, of the fact that…