Une formalisation des faisceaux et des schémas affines en théorie des types avec Coq / A formalization of affine bundle and schemes in type theory with Coq

CHICLI, Laurent

In: JFLA 2001 : journées francophones des langages applicatifs (Pontcarlier, 29-30 janvier 2001 ) :17-31

Konferenz - print, 9 ref

Nous présentons nos spécifications en théorie des types des notions mathématiques nécessaires à la définition des schémas affines, l'un des premiers éléments de la géométrie algébrique moderne. Pour cela topologie et théorie des faisceaux ont étés développées, nous décrivons ici leurs spécifications, ainsi que les problèmes rencontrés lors de ce travail.

Titel:	Une formalisation des faisceaux et des schémas affines en théorie des types avec Coq / A formalization of affine bundle and schemes in type theory with Coq
Autor/in / Beteiligte Person:	CHICLI, Laurent
Link:	View record from PASCAL Archive
Quelle:	JFLA 2001 : journées francophones des langages applicatifs (Pontcarlier, 29-30 janvier 2001 ) :17-31
Veröffentlichung:	Le Chesnay: INRIA, 2001
Medientyp:	Konferenz
Umfang:	print, 9 ref
Schlagwort:	Computer science Informatique Sciences exactes et technologie Exact sciences and technology Sciences appliquees Applied sciences Informatique; automatique theorique; systemes Computer science; control theory; systems Informatique théorique Theoretical computing Algorithmique. Calculabilité. Arithmétique ordinateur Algorithmics. Computability. Computer arithmetics Démonstration automatique Automatic proving Demostración automática Géométrie algébrique Algebraic geometry Geometría algebraica Théorie type Type theory Vérification programme Program verification Verificación programa Coq
Sonstiges:	Nachgewiesen in: PASCAL Archive Sprachen: French Original Material: INIST-CNRS Document Type: Conference Paper File Description: text Language: French Author Affiliations: INRIA Sophia-Antipolis, Projet Lemme, France Rights: Copyright 2002 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

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.