Skip to Main content Skip to Navigation
Conference papers

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

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/inria-00432525
Contributor : Arnaud Spiwack <>
Submitted on : Monday, November 16, 2009 - 3:43:36 PM
Last modification on : Thursday, June 18, 2020 - 10:18:03 AM
Long-term archiving on: : Thursday, June 17, 2010 - 6:08:07 PM

File

v2.pdf
Files produced by the author(s)

Identifiers

Collections

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⟩

Share

Metrics

Record views

629

Files downloads

554