Related papers: Revisiting the Fast Fourier Transform in Rocq
It is well known in the Constraint Programming community that any non-binary constraint satisfaction problem (with finite domains) can be transformed into an equivalent binary one. One of the most well-known translations is the Hidden…
In this article we present a method for formally proving the correctness of the lazy algorithms for computing homographic and quadratic transformations -- of which field operations are special cases-- on a representation of real numbers by…
A recent generalization of the Central Limit Theorem consistent with nonextensive statistical mechanics has been recently achieved through a generalized Fourier transform, noted $q$-Fourier transform. A representation formula for the…
The Coq Platform is a continuously developed distribution of the Coq proof assistant together with commonly used libraries, plugins, and external tools useful in Coq-based formal verification projects. The Coq Platform enables reproducing…
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…
The $p$-adic $q$-integral (= $I_q$-integral) was defined by author in the previous paper [1, 3]. In this paper, we consider $I_q$-Fourier transform and investigate some properties which are related to this transform.
Image computation is a fundamental tool for performance assessment of astronomical instrumentation, usually implemented by Fourier transform techniques. We review the numerical implementation, evaluating a direct implementation of the…
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…
Current approaches for formal verification of algorithms face important limitations. For specification, they cannot express algorithms naturally and concisely, especially for algorithms with states and flexible control flow. For…
We consider the recursive Fourier sampling problem (RFS), and show that there exists an interactive proof for RFS with an efficient classical verifier and efficient quantum prover.
The Replica Fourier Transform introduced previously is related to the standard definition of Fourier transforms over a group. Its use is illustrated by block-diagonalizing the eigenvalue equation of a four-replica Parisi matrix.
We exploit (co)inductive specifications and proofs to approach the evaluation of low-level programs for the Unlimited Register Machine (URM) within the Coq system, a proof assistant based on the Calculus of (Co)Inductive Constructions type…
The ever-growing complexity of mathematical proofs makes their manual verification by mathematicians very cognitively demanding. Autoformalization seeks to address this by translating proofs written in natural language into a formal…
Based on the definition of the Fourier transform in terms of the number operator of the quantum harmonic oscillator and in the corresponding definition of the fractional Fourier transform, we have obtained the discrete fractional Fourier…
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…
For a sample set of 1024 values, the FFT is 102.4 times faster than the discrete Fourier transform (DFT). The basis for this remarkable speed advantage is the `bit-reversal' scheme of the Cooley-Tukey algorithm. Eliminating the burden of…
The Lax Logical Framework, LLFP, was introduced, by a team including the last two authors, to provide a conceptual framework for integrating different proof development tools, thus allowing for external evidence and for postponing,…
The FFT algorithm that implements the discrete Fourier transform is considered one of the top ten algorithms of the $20$th century. Its main strengths are the low computational cost of $\mathcal{O}(n \log n$) and its stability. It is one of…
In order to increase user confidence, many automated theorem provers provide certificates that can be independently verified. In this paper, we report on our progress in developing a standalone tool for checking the correctness of…
We investigate here a new version of the Calculus of Inductive Constructions (CIC) on which the proof assistant Coq is based: the Calculus of Congruent Inductive Constructions, which truly extends CIC by building in arbitrary first-order…