Towards Constructive Homological Algebra in Type Theory

Thierry Coquand 1 Arnaud Spiwack 2, 3
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 : jeudi 10 mai 2018 - 02:06:54
Document(s) archivé(s) le : jeudi 17 juin 2010 - 18:08:07

Fichier

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

Identifiants

Collections

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〉

Partager

Métriques

Consultations de la notice

477

Téléchargements de fichiers

213