Einzeltreffer — DigiBib

We program the Fast Fourier Transform in type theory, using the tool Coq. We prove its correctness and the correctness of the Inverse Fourier Transform. A type of trees representing vectors with interleaved elements is defined to facilitate the definition of the transform by structural recursion. We define several operations and proof tools for this data structure, leading to a simple proof of correctness of the algorithm. The inverse transform, on the other hand, is implemented on a different representation of the data, that makes reasoning about summations easier. The link between the two data types is given by an isomorphism. This work is an illustration of the two-level approach to proof development and of the principle of adapting the data representation to the specific algorithm under study. CtCoq, a graphical user interface of Coq, helped in the development. We discuss the characteristics and usefulness of this tool.

Titel:	Certifying the Fast Fourier Transform with coq
Autor/in / Beteiligte Person:	CAPRETTA, Venanzio
Link:	E-Journal im Bestand der UB Hagen? View record from PASCAL Archive
Quelle:	TPHOLs 2001 : theorem proving in higher order logics (Edinburgh, 3-6 September 2001)Lecture notes in computer science :154-168
Veröffentlichung:	Berlin: Springer, 2001
Medientyp:	Konferenz
Umfang:	print, 11 ref
ISSN:	0302-9743 (print)
Schlagwort:	Computer science Informatique Mathematics Mathématiques Sciences exactes et technologie Exact sciences and technology Sciences et techniques communes Sciences and techniques of general use Mathematiques Logique mathématique, fondements, théorie des ensembles Mathematical logic, foundations, set theory Logique et fondements Logic and foundations Théorie de la preuve et mathématiques constructives Proof theory and constructive mathematics Sciences appliquees Applied sciences Informatique; automatique theorique; systemes Computer science; control theory; systems Informatique théorique Theoretical computing Généralités General Démonstration théorème Theorem proving Demostración teorema Isomorphisme Isomorphism Isomorfismo Structure donnée Data structure Estructura datos Théorie type Type theory Transformation Fourier rapide Fast Fourier transformation Transformación Fourier rápida Transformation inverse Inverse transformation Transformación inversa COQ
Sonstiges:	Nachgewiesen in: PASCAL Archive Sprachen: English Original Material: INIST-CNRS Document Type: Conference Paper File Description: text Language: English Author Affiliations: Computing Science Institute, University of Nijmegen, Postbus 9010, 6500 GL Nijmegen, Netherlands Rights: Copyright 2001 INIST-CNRS ; CC BY 4.0 ; Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS Notes: Computer science; theoretical automation; systems ; Mathematics

Klicken Sie ein Format an und speichern Sie dann die Daten oder geben Sie eine Empfänger-Adresse ein und lassen Sie sich per Email zusenden.

BibTeX Citavi, JabRef, u.a.
(Literaturverwaltung)

PDF kein Volltext!
(Merkzettel, Notizen)

RIS Endnote, Citavi u.a.
(Literaturverwaltung)

MODS
(XML zur Weiterverarbeitung)

oder

Wählen Sie das für Sie passende Zitationsformat und kopieren Sie es dann in die Zwischenablage, lassen es sich per Mail zusenden oder speichern es als PDF-Datei.

Gewünschter Zitations-Stil:

oder

Bitte prüfen Sie, ob die Zitation formal korrekt ist, bevor Sie sie in einer Arbeit verwenden. Benutzen Sie gegebenenfalls den "Exportieren"-Dialog, wenn Sie ein Literaturverwaltungsprogramm verwenden und die Zitat-Angaben selbst formatieren wollen.

Certifying the Fast Fourier Transform with coq