Recent Changes - Search:

ForMath Main

Project Pages

Internal Pages

edit SideBar

ForMath /

Papers and Slides

Table of contents:

Publications in Journals, Conferences and Workshops

  • March 2013: The Picard Algorithm for Ordinary Differential Equations in Coq, Evgeny Makarov and Bas Spitters, Rough Diamond, ITP2013 PDF, 2013.
  • February 2013: The Role of Formalization in Computational Mathematics, Julio Rubio. Accepted for publication in Bulletin Belgian Mathematical Society (BBMS). 2013.
  • February 2013: Type classes for efficient exact real arithmetic in Coq Robbert Krebbers and Bas Spitters, LMCS 1106.3448 DOI, 9(1:1), 2013.
  • February 2013: Computing Persistent Homology within Coq/SSReflect, J. Heras, T. Coquand, A. Mörtberg and V. Siles. Accepted for publication in ACM Transactions on Computational Logic (TOCL); PDF; Arxiv version. 2013.
  • February 2013: Matrices ŕ blocs et en forme canonique, G. Cano and M. Dénčs. JFLA - Journées francophones des langages applicatifs; PDF. 2013.
  • January 2013: Rank Nullity theorem in Linear Algebra, Jose Divasón and Jesús Aransay, published in Archive of Formal Proofs; AFP entry. 2013.
  • December 2012 Coherent and Strongly Discrete Rings in Type Theory, T. Coquand, A. Mörtberg and V. Siles. CPP 2012, DOI link, PDF.
  • September 2012 A Formal Proof of Sasaki-Murao Algorithm, T. Coquand, A. Mörtberg and V. Siles. Journal of Formalized Reasoning, vol 5, No 1. To PDF.
  • August 2012 A Refinement-Based Approach to Computational Algebra in Coq, M. Dénčs, A. Mörtberg and V.Siles ITP 2012, Lecture Notes in Computer Science. DOI link, PDF.
  • August 2012 Construction of real algebraic numbers in Coq, C. Cohen ITP 2012, Lecture Notes in Computer Science. DOI link, PDF.
  • August 2012 A language of patterns for subterm selection, G. Gonthier and E. Tassi. ITP 2012, Lecture Notes in Computer Science, 7406, pages 361--376, 2012. DOI link PDF.
  • July 2012: Verifying an algorithm computing Discrete Vector Fields for digital imaging, J. Heras, M. Poza, and J. Rubio. Calculemus 2012, Lecture Notes in Computer Science, 7362, pages 215--229, 2012. PDF, DOI link, Arxiv link.
  • May 2012: Towards a certi fied computation of homology groups for digital images, J. Heras, M. Dénčs, G. Mata, A. Mörtberg, M. Poza, and V. Siles. CTIC 2012, Lecture Notes in Computer Science, 7309, pages 49--57, 2012. PDF, DOI link.
  • March 2012: Computer-assisted proof (Text in Spanish. Demostración asistida por ordenador), J.M. Aransay and C. Domínguez. La Gaceta de la Real Sociedad Matemática Espańola, 15(1), 2012, pp.75-104. RSME 2012
  • February 2012 A constructive proof of Simpson's Rule, Thierry Coquand and Bas Spitters. Logic and Analysis 4:15 pp1-8 DOI 1202.3460 2012.
  • February 2012: A constructive version of Laplace’s proof on the existence of complex roots, C. Cohen and T. Coquand. Preprint. In Journal of Algebra, volume 381, Pages 110–115. To appear in May 2013. DOI.
  • February 2012: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination Cyril Cohen and Assia Mahboubi. Logical Methods in Computer Science, volume 8, issue 1, paper 2, 2012. PDF DOI link.
  • February 2012: A Certified Module to Study Digital Images with the Kenzo System. J. Heras,V. Pascual and J. Rubio. Lecture Notes in Computer Science, 6927, pages 113--120, 2012. Springer-Verlag. PDF, DOI link.
  • January 2012: Formalization of a Normalization Theorem in Simplicial Topology . L. Lambán, F. J. Martín-Mateos, J. L. Ruiz-Reina, J. Rubio. Annals of Mathematics and Artificial Intelligence 64(1), 2012, pp. 1--37. PDF. DOI Link.
  • December 2011: On automation and certification of a homological method to process biomedical digital images, J. Heras, G. Mata, M. Poza, and J. Rubio. ImageN-A 2(4), 2011, pp. 29--31. PDF. ImageN-A Link
  • December 2011: A Decision Procedure for Regular Expression Equivalence in Type Theory, Thierry Coquand and Vincent Siles. CPP'11. PDF Coq/SSReflect development. DOI Link.
  • August 2011: Point-free, set-free concrete linear algebra. G. Gonthier. ITP 2011, Lecture Notes in Computer Science, 6898, pp. 103-118. PDF. DOI Link.
  • August 2011: Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials. L. Lambán, F. J. Martín-Mateos, J. L. Ruiz-Reina, J. Rubio. ITP'11. Lecture Notes in Computer Science, 6898, pages 200--215, 2011. PDF. DOI Link. ACL2 development.
  • August 2011: A formal study of Bernstein coefficients and polynomials Yves Bertot, Frederique Guilhot, Assia Mahboubi, Mathematical Structures in Computer Sciences 21(4), 2011, pp. 731-761. DOI Link, preprint.
  • August 2011: Type classes for Mathematics in Type Theory, Bas Spitters and Eelis van der Weegen. Mathematical Structures in Computer Sciences 21(4), 2011, pp. 795 - 825 DOI Link, ArXiv 1102.1323. Coq development.
  • August 2011: Formal Proofs for Theoretical Properties of Newton's Method. Ioana Pasca, Mathematical Structures in Computer Sciences 21(4), 2011, pp. 683-714. DOI Link, preprint.
  • July 2011: Incidence simplicial matrices formalized in Coq/SSReflect. J. Heras, M. Poza, M. Dénčs and L. Rideau. CICM'11. Lecture Notes in Computer Science, 6824, pages 30--44, 2011. PDF. DOI Link. Coq/SSReflect development.
  • July 2011: Computer certified efficient exact reals in Coq Robbert Krebbers and Bas Spitters, CICM'11 LNCS (2011) Vol 6824/2011, 90-106. 1105.2751 PDF sources DOI link.
  • March 2011: Effective homology of bicomplexes, formalized in Coq. C. Domínguez and J. Rubio. Theoretical Computer Science 412, pages 962-970, 2011. Attach:EHBFC. DOI link
  • February 2011: Proving with ACL2 the correctness of simplicial sets in the Kenzo system. J. Heras,V. Pascual and J. Rubio. Lecture Notes in Computer Science, 6564, pages 37--51, 2011. Springer-Verlag. Attach:lopstr2010-lncs, DOI link.
  • September 2010: An introduction to small scale reflection in Coq Georges Gonthier, Assia Mahboubi, PDF, Journal of Formalized Reasoning, vol 3, No2.
  • September 2010: Generating certified code from formal proofs: a case study in Homological Agebra Jesús Aransay, Julio Rubio and Clemens Ballarin, abstract at PROLE2010.
  • July 2010: Proving with ACL2 the correctness of simplicial sets in the Kenzo system. J. Heras,V. Pascual and J. Rubio. In Proceedings LOPSTR 2010. LOPSTR pre-proceedings
  • 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, DOI link.
  • 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, DOI link.
  • July 2010: Formally Verified Conditions for Regularity of Interval Matrices Ioana Pasca, preprint, at Calculemus 2010, DOI link.
  • July 2010: Computing in Coq with Infinite Algebraic Data Structures. C. Domínguez and J. Rubio. In Calculemus 2010, LNCS 6167, pages 204-218, Springer-Verlag. Free access version, DOI link.
  • July 2010: A formal quantifier elimination for algebraically closed fields Cyril Cohen, Assia Mahboubi, preprint, at Calculemus 2010, DOI link.



Thesis, Technical Reports and Preprints

  • March 2013 A Hierarchy of mathematical structures in ACL2, J. Heras, F.J. Martín-Mateos and V. Pascual, PDF. web.
  • February 2013 A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and OCL2, J. Aransay, J. Divasón, J. Heras, L. Lambán, V. Pascual, A.L. Rubio, J. Rubio, PDF
  • November 2012 Formalized algebraic numbers: construction and first-order theory, C. Cohen, PhD Thesis, École Polytechnique (France) PDF
  • June 2012: Report on J. Heras stay in Göteborg, J. Heras, PDF.
  • October 2011: Proofs of properties of finite-dimensional vector spaces in Isabelle/HOL, J. Divasón. Degree's Thesis, PDF, sources.
  • July 2011: Type classes for efficient exact real arithmetic in Coq Robbert Krebbers and Bas Spitters, 1106.3448 sources.
  • June 2011: Homological processing of biomedical digital images: automation and certification, J. Heras, G. Mata, M. Poza, and J. Rubio. Technical Report. PDF.
  • May 2011: Mathematical Knowledge Management in Algebraic Topology, Jónathan Heras, PhD Thesis, University of La Rioja. (Thesis, Author web, Permanent link).
  • February 2011: From Digital Images to Simplicial Complexes: A report. Technical report by ForMath La Rioja node. Attach:fditscr
  • February 2011: A certified module of Simplicial Complexes for the Kenzo system. Technical report by J. Heras, V. Pascual and J. Rubio. Attach:acmoscftks-lncs
  • November 2010: Formal Verification for Numerical Methods, Ioana Pasca, PhD Thesis, University of Nice Sophia Antipolis. Author version.
  • August 2010: Hybrid System veri cation in Coq, report of Hugo Férée's research visit at Radbound University, directed by Herman Geuvers (pdf, code)
  • July 2010: When first order is enough: the case of Simplicial Topology. L. Lambán, F. J. Martín-Mateos, J. L. Ruiz-Reina, J. Rubio. Technical report. Attach:wfoe
  • 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
Edit - History - Print - Recent Changes - Search
Page last modified on May 20, 2013, at 04:33 PM