Skip to Main content Skip to Navigation
Conference papers

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
Abstract : This paper reports on ongoing work on the project of representing the Kenzo system in type theory.
Document type :
Conference papers
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download
https://hal.inria.fr/inria-00432525
Contributor : Arnaud Spiwack Connect in order to contact the contributor
Submitted on : Monday, November 16, 2009 - 3:43:36 PM
Last modification on : Friday, February 4, 2022 - 3:08:57 AM
Long-term archiving on: : Thursday, June 17, 2010 - 6:08:07 PM

File

Vignette du document
v2.pdf
Files produced by the author(s)

Identifiers

Collections

X | CNRS | INRIA | LIX | INSMI | X-LIX | X-DEP-INFO | INRIA2

Citation

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

Export

BibTeX TEI DC DCterms EndNote Datacite

Share

Metrics

Record views

272

Files downloads

354

 

Contact                    Legal Notice                    Personal Data