Towards Constructive Homological Algebra in Type Theory

Thierry Coquand 1 Arnaud Spiwack 2, 3
1 Division of Computing Science
2 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
3 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : This paper reports on ongoing work on the project of representing the Kenzo system in type theory.
Type de document :
Communication dans un congrès
CALCULEMUS 2007, Jun 2007, Hagenberg, Austria. 12 p., 2007, 〈10.1007/978-3-540-73086-6_4〉
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00432525
Contributeur : Arnaud Spiwack <>
Soumis le : lundi 16 novembre 2009 - 15:43:36
Dernière modification le : mercredi 25 avril 2018 - 10:45:26
Document(s) archivé(s) le : jeudi 17 juin 2010 - 18:08:07

Fichier

v2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | LIX | INSMI | X-LIX | X | PARISTECH

Citation

Thierry Coquand, Arnaud Spiwack. Towards Constructive Homological Algebra in Type Theory. CALCULEMUS 2007, Jun 2007, Hagenberg, Austria. 12 p., 2007, 〈10.1007/978-3-540-73086-6_4〉. 〈inria-00432525〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

426

Téléchargements de fichiers

193

Contact


archive-ouverte@inria.fr