- 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