Related papers: Coinductive Formal Reasoning in Exact Real Arithme…
Computational content encoded into constructive type theory proofs can be used to make computing experiments over concrete data structures. In this paper, we explore this possibility when working in Coq with chain complexes of infinite type…
Reasoning about real number expressions in a proof assistant is challenging. Several problems in theorem proving can be solved by using exact real number computation. I have implemented a library for reasoning and computing with complete…
Solutions to differential equations, which are used to model physical systems, are computed numerically by solving a set of discretized equations. This set of discretized equations is reduced to a large linear system, whose solution is…
A quantum circuit is a computational unit that transforms an input quantum state to an output one. A natural way to reason about its behavior is to compute explicitly the unitary matrix implemented by it. However, when the number of qubits…
We describe an embedding of the QWIRE quantum circuit language in the Coq proof assistant. This allows programmers to write quantum circuits using high-level abstractions and to prove properties of those circuits using Coq's theorem proving…
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…
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:…
Formal proof checkers such as Coq are capable of validating proofs of correction of algorithms for finite field arithmetics but they require extensive training from potential users. The delayed solution of a triangular system over a finite…
interpreters are tools to compute approximations for behaviors of a program. These approximations can then be used for optimisation or for error detection. In this paper, we show how to describe an abstract interpreter using the type-theory…
We propose abstract compilation for precise static type analysis of object-oriented languages based on coinductive logic programming. Source code is translated to a logic program, then type-checking and inference problems amount to queries…
This article revisits standard theorems from elementary number theory from a constructive, algorithmic, and proof-theoretic perspective, framed within the theory of computable functionals TCF. Key examples include B\'ezout's identity, the…
Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to formalizing homotopy-theoretic…
In functional programming, datatypes a la carte provide a convenient modular representation of recursive datatypes, based on their initial algebra semantics. Unfortunately it is highly challenging to implement this technique in proof…
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 propose a new library to model and verify hardware circuits in the Coq proof assistant. This library allows one to easily build circuits by following the usual pen-and-paper diagrams. We define a deep-embedding: we use a (dependently…
We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a simple quantum intermediate…
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…
Context-free language theory is a well-established area of mathematics, relevant to computer science foundations and technology. This paper presents the preliminary results of an ongoing formalization project using context-free grammars and…
The "Concrete Semantics" book gives an introduction to imperative programming languages accompanied by an Isabelle/HOL formalization. In this paper we discuss a re-formalization of the book using the Coq proof assistant. In order to achieve…
The implementation and practicality of quantum algorithms highly hinge on the quality of operations within a quantum processor. Therefore, including realistic error models in quantum computing simulation platforms is crucial for testing…