Abstract
This paper reports on ongoing work on the project of representing the Kenzo system [15] in type theory [11].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aransay, J.M.: Razonamiento mecanizado en álgebra homológica. PhD thesis (2006)
Artin, M., Grothendieck, A., Verdier, J,-L.: Univers Séminaire de Géométrie Algébrique du Bois Marie -,1963-64 - Théorie des topos et cohomologie étale des schémas - (SGA 4) - vol. 1, LNM 269, 185-217, Springer-Verlag, Berlin, New York (1963)
Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill, New York (1967)
de Bruijn, N.G.: Telescopic mappings in typed lambda calculus. Inform. and Comput. 91(2), 189–204 (1991)
Barakat, M., Robertz, D.: homalg: First steps to an abstract package for homological algebra. In: Proceedings of the X meeting on computational algebra and its applications (EACA 2006), Sevilla, Spain, pp. 29–32 (2006)
LogiCal project. The Coq Proof Assistant (2007), http://coq.inria.fr/V8.1/refman/index.html
Coquand, T.: Metamathematical investigations of a calculus of constructions. Rapport de recherche de l’INRIA (1989)
Gregoire, B., Leroy, X.: A Compiled Implementation of Strong Reduction. International Conference on Functional Programming (2002)
Huet, G., Saibi, A.: Constructive category theory. In: Proof, language, and interaction. Found. Comput. Ser., pp. 239–275. MIT Press, Cambridge, MA (2000)
Landin, P.: The mechanical evaluation of expressions. Comput. J. 6, 308–320 (1964)
Martin-Löf, P.: An intuitionistic theory of types. In: Twenty-five years of constructive type theory (Venice, 1995), pp. 127–172, Oxford Logic Guides, 36, Oxford Univ. Press, New York (1998)
Melliès, P.-A., Werner, B.: A Generic Normalization Proof for Pure Type Systems. In: Paulin-Mohring, C., Gimenez, E. (eds.) TYPES 1996. LNCS, Springer, Heidelberg (1997)
Miquel, A., Werner, B.: The Not So Simple Proof-Irrelevant Model of CC. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, Springer, Heidelberg (2003)
Mines, R., Richman, F., Ruitenburg, W.: A Course in Constructive Algebra. Springer, Heidelberg (1988)
Rubio, J., Sergereart, F.: Constructive Homological Algebra and Applications, Genove Summer School (2006), available at http://www-fourier.ujf-grenoble.fr/~sergerar/Papers/
Spiwack, A.: Ajouter des entiers machine à Coq. Master thesis, http://arnaud.spiwack.free.fr/
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coquand, T., Spiwack, A. (2007). Towards Constructive Homological Algebra in Type Theory. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds) Towards Mechanized Mathematical Assistants. MKM Calculemus 2007 2007. Lecture Notes in Computer Science(), vol 4573. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73086-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-73086-6_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73083-5
Online ISBN: 978-3-540-73086-6
eBook Packages: Computer ScienceComputer Science (R0)