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 veri cation 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.