ForMath Main
Project Pages
Internal Pages
edit SideBar

Publications
 Effective homology of bicomplexes, formalized in Coq. C. Domínguez and J. Rubio. Theoretical Computer Science 412, pages 962970, 2011.
 When first order is enough: the case of Simplicial Topology. L. Lambán, F. J. MartínMateos, J. L. RuizReina, 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 204218, SpringerVerlag. 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. SpringerVerlag. LOPSTR preproceedings
 July 2010: Automated MachineChecked Hybrid System Safety Proofs Herman Geuvers, Dan Synek, Adam Koprowski, Eelis van der Weegen at ITP10. PDF and development.
 July 2010: Developing the algebraic hierarchy with type classes in Coq Bas Spitters and Eelis van der Weegen. Rough Diamond at ITP10. 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
Slides
