Construction des nombres algébriques réels en Coq

Cohen, Cyril ; Symbolic Special Functions : Fast and Certified (SPECFUN) ; et al.

In: JFLA-Journées Francophones des Langages Applicatifs-2012 JFLA-Journées Francophones des Langages Applicatifs-2012, Feb 2012, Carnac, France Cyril Cohen; (2012-02-04)

Online unknown

Wie komme ich dran?

Zugriff:

View record in OpenAIRE (Volltext)

National audience; Cet article présente une construction en Coq de l'ensemble des nombres algébriques réels, ainsi qu'une preuve formelle que cet ensemble est muni d'une structure de corps réel clos discret archimédien. Cette construction vient ainsi implémenter une interface de corps réel clos réalisée dans un travail antérieur et bénéficie alors de la propriété d'élimination des quantificateurs, formellement prouvée pour toute instance de l'interface. Ce travail est destiné à servir de fondement à une construction de l'ensemble des nombres algébriques complexes, ainsi que d'implémentation de référence pour la certification des nombreux algorithmes de calcul formel qui utilisent des nombres algébriques.

Titel:	Construction des nombres algébriques réels en Coq
Autor/in / Beteiligte Person:	Cohen, Cyril ; Symbolic Special Functions : Fast and Certified (SPECFUN) ; Inria Saclay - Ile de France ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) ; Microsoft Research - Inria Joint Centre (MSR - INRIA) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Microsoft Research Laboratory Cambridge-Microsoft Corporation [Redmond, Wash.] ; Types, Logic and computing (TYPICAL) ; Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX) ; École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France ; École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)
Link:	View record in OpenAIRE (Volltext) https://inria.hal.science/hal-00665965/document
Quelle:	JFLA-Journées Francophones des Langages Applicatifs-2012 JFLA-Journées Francophones des Langages Applicatifs-2012, Feb 2012, Carnac, France Cyril Cohen; (2012-02-04)
Veröffentlichung:	HAL CCSD, 2012
Medientyp:	unknown
Schlagwort:	[INFO.INFO-OH]Computer Science [cs]/Other [cs.OH]
Sonstiges:	Nachgewiesen in: OpenAIRE Sprachen: French Language: French

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.