ForMath /

# Publications and Slides

## Publications

*Effective homology of bicomplexes, formalized in Coq*. C. Domínguez and J. Rubio. Theoretical Computer Science 412, pages 962-970, 2011.*When first order is enough: the case of Simplicial Topology*. L. Lambán, F. J. Martín-Mateos, J. L. Ruiz-Reina, J. Rubio. Preprint, submitted. Attach:wfoe**September 2010:***An introduction to small scale reflection in Coq*Georges Gonthier, Assia Mahboubi, preprint, submitted.**July 2010:***A formal study of Bernstein coefficients and polynomials*Yves Bertot, Frederique Guilhot, Assia Mahboubi, preprint, submitted.**July 2010:***A formal quantifier elimination for algebraically closed fields*Cyril Cohen, Assia Mahboubi, preprint, at Calculemus 2010.**July 2010:***Formally Verified Conditions for Regularity of Interval Matrices*Ioana Pasca, preprint, at Calculemus 2010.**July 2010:***Computing in Coq with Infinite Algebraic Data Structures*. C. Domínguez and J. Rubio. In Calculemus 2010, Lecture Notes in Artificial Intelligence, 6167, pages 204-218, Springer-Verlag. Free access version.**July 2010:***Proving with ACL2 the correctness of simplicial sets in the Kenzo system*. J. Heras,V. Pascual and J. Rubio. In LOPSTR 2010, Lecture Notes in Computer Science. Springer-Verlag. LOPSTR pre-proceedings**July 2010:***Automated Machine-Checked Hybrid System Safety Proofs*Herman Geuvers, Dan Synek, Adam Koprowski, Eelis van der Weegen at ITP-10. PDF and development.**July 2010:***Developing the algebraic hierarchy with type classes in Coq*Bas Spitters and Eelis van der Weegen. Rough Diamond at ITP-10. PDF and development.*Type Classes For Mathematics in Coq*Bas Spitters and Eelis van der Weegen. Submitted for publication. PDF and development.

## Thesis and Technical Reports

**June 2010:***Report on a SSReflect week*. Technical report by Yves Bertot, Laurence Rideau and ForMath La Rioja node. Attach:SSReflectWeekLaRioja**May 2010:***Constructive Algebra in Functional Programming and Type Theory*. Master thesis by Anders Mörtberg. Here is a text describing informally what Anders has represented.

## Slides

**May 2010:**J. Rubio.*Mechanising mathematics: the case of Algebraic Topology*. Invited talk at the Conference in honor of Tomas Recio.http://www.trecio60th.unican.es/. Attach:TomasTalk.**April 2010:**J. Heras and V. Pascual.*ACL2 verication of Simplicial Complexes programs for the Kenzo system*. Workshop on Algebraic computing, soft computing, and program verification. http://www.gimac.uma.es/hard&soft2010/Home.html. Attach:avoscpitks.**April 2010:**J. Aransay.*Living (i.e. executing and proving) with different representations of datatypes*. Workshop on Algebraic computing, soft computing, and program verification. http://www.gimac.uma.es/hard&soft2010/Home.html. Attach:lwdrod.pdf.- J. Heras, V. Pascual and J. Rubio.
*Proving with ACL2 the correctness of simplicial sets in the Kenzo system*. 20th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2010. http://www.risc.jku.at/about/conferences/lopstr2010/index.html. Attach:lopstr2010.