Four Approaches to Automated Reasoning with Differential Algebraic Structures - Artificial Intelligence and Symbolic Computation - page 235

4. In order to develop algebraic topology, one of the basic concepts needed (see
definitions in Section 2) is infinite complexes (of modules, for instance). Some
attempts have been made to produce an implementation of them (see [8]),
but definitive results have not been obtained yet. For their implementation,
lazy lists or extensible records might be used, but these ideas will be studied
in future work.
Acknowledgements
We are grateful to Wolfgang Windsteiger and the anonymous referees for the
useful comments on the previous version of this paper.
References
1. C. Ballarin, Locales and Locale Expressions in Isabelle/Isar . In Stefano Berardi et
al., TYPES 2003, LNCS vol. 3085, pp. 34 - 50.
2. S. Berghofer, Program Extraction in Simply-Typed Higher Order Logic , TYPES
2002, LNCS vol. 2646, pp. 21-38
3. R. Brown, The twisted Eilenberg-Zilber theorem , Celebrazioni Arch. Secolo XX,
Simp. Top. (1967), pp. 34-37.
4. J. Calmet, Some Grand Mathematical Challenges in Mechanized Mathematics ,In
T. Hardin and Renaud Rioboo, editors, Calculemus 2003, pp. 137 - 141.
5. X. Dousson, F. Sergeraert and Y. Siret, The Kenzo program ,
http://www-fourier.ujf-grenoble.fr/˜sergerar/Kenzo/
6. J. Glimming, Logic and Automation for Algebra of Programming , Master Thesis,
Maths Institute, University of Oxford, August 2001, available at
http://www.nada.kth.se/˜glimming/publications.shtml.
7. V. K. A. M. Gugenheim, On the chain complex of a fibration , Illinois Journal of
Mathematics 16 (1972), pp. 398-414.
8. H. Kobayashi, H. Suzuki and H. Murao, Rings and Modules in Isabelle/HOL ,In
T. Hardin and Renaud Rioboo, editors, Calculemus 2003, pp. 124 - 129.
9. L. Lamban, V. Pascual and J. Rubio, An object-oriented interpretation of the EAT
system , Appl. Algebra Eng. Commun. Comput. vol. 14(3) pp. 187-215.
10. S. Mac Lane, Homology , Springer, 1994.
11. W. Naraschewski and M. Wenzel, Object-Oriented Verification based on Record
Subtyping in Higher-Order Logic , In J. Grundy and M. Newey, editors, TPHOLs'98,
LNCS vol. 1479, pp. 349-366.
12. T. Nipkow, L. C. Paulson and M. Wenzel, Isabelle/HOL: A proof assistant for
higher order logic , LNCS vol. 2283, 2002.
13. L. Paulson, Defining Functions on Equivalence Classes , Report available at
http://www.cl.cam.ac.uk/users/lcp/papers/Reports/equivclasses.pdf
14. J. Rubio and F. Sergeraert, Constructive Algebraic Topology , Lecture Notes Sum-
mer School in Fundamental Algebraic Topology, Institut Fourier, 1997.
15. J. Rubio, F. Sergeraert and Y. Siret, EAT: Symbolic Software for Effective Homol-
ogy Computation , Institut Fourier, Grenoble, 1997.
16. W. Shih, Homologie des espaces fibres , Publications Mathematiques de l'I.H.E.S.
13, 1962.
17. L. Thery, Proving and computing: A certified version of the Buchberger's algo-
rithm , in Proceeding of the 15th International Conference on Automated Deduc-
tion, LNAI vol. 1421, 1998.