une formalisation des faisceaux et des schémas affines en théorie des types avec Coq

Laurent Chicli 1
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : On présente ici un début de formalisation de la géométrie algébrique en théorie des types avec la définition des schémas affines. Pour cela topologie, algèbre et théorie des faisceaux ont étés développées en Coq, nous décrivons leurs spécifications, ainsi que les problèmes rencontrés lors de ce travail.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00072403
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 9:52:01 AM
Last modification on : Saturday, January 27, 2018 - 1:31:07 AM
Long-term archiving on: Sunday, April 4, 2010 - 11:06:08 PM

Identifiers

  • HAL Id : inria-00072403, version 1

Collections

Citation

Laurent Chicli. une formalisation des faisceaux et des schémas affines en théorie des types avec Coq. RR-4216, INRIA. 2001. ⟨inria-00072403⟩

Share

Metrics

Record views

172

Files downloads

155