Mörtberg, Anders; Dénès, Maxime; Siles, Vincent: A Refinement-Based Approach to Computational Algebra in Coq. Lennart Beringer, Amy P. Felty (Eds.): Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings. Lecture Notes in Computer Science , 2012 (7406) pp. 83-98. ISBN/ISSN: 978-3-642-32346-1

Mörtberg, Anders; Coquand, Thierry; Siles, Vincent: Coherent and Strongly Discrete Rings in Type Theory. CPP 2012, LNCS , 7679 pp. 273-288.

Mörtberg, Anders: Constructive Algebra in Type Theory. Göteborg : University of Gothenburg.

Mörtberg, Anders; Siles, Vincent; Heras, Jónathan; Dénès, Maxime; Mata, Gadea; Poza, María: Towards a Certified Computation of Homology Groups for Digital Images. Massimo Ferri, Patrizio Frosini, Claudia Landi, Andrea Cerri, Barbara Di Fabio (Eds.): Computational Topology in Image Context - 4th International Workshop, CTIC 2012, Bertinoro, Italy, May 28-30, 2012. Proceedings. Lecture Notes in Computer Science , 2012 (7309) pp. 49-57. ISBN/ISSN: 978-3-642-30237-4