On Friday 22/11/2013, at 10h30, in room Byron Beige,

**Speaker:** Cyril Cohen.

**Joint work with:** Anders Mortberg.

**Title:** A Coq formalization of finitely presented modules.

Abstract:

The use of vector spaces in homology theory does not give as precise

information as with modules. A generalization to finitely presented modules

covers computable Z-homology, which gives finer-grained topological invariants.

We formalize a construction of finitely presented modules over coherent and

strongly discrete rings and discuss its properties. This formalization gives

basic building blocks that lead to a clean definition of homology groups.