ForMath Main
Project Pages
Internal Pages
edit SideBar

Table of contents:
Publications in Journals, Conferences and Workshops
 April 2014 A certified reduction strategy for homological image processing, M. Poza, C. Domínguez, J. Heras and J. Rubio. Accepted for publication in ACM Transactions on Computational Logic. Paper.
 September 2013 Theorem of 3 circles in Coq, Julianna Zsidó. Accepted for publication (after modifications) in Journal of Automated Resasoning, ArXiv version. DOI link.
 August 2013 Refinements for free!, C. Cohen, M. Dénčs and A. Mörtberg. Accepted for publication in CPP 2013, PDF. DOI link.
 July 2013 Formalization and execution of Linear Algebra: from theorems to algorithms, J. Aransay and J. Divasón. Accepted for publication in LOPSTR 2013, Madrid, 2013. PDF.
 July 2013 Performance Analysis of a Verified Linear Algebra Program in SML, J. Aransay and J. Divasón. TPF 2013, Madrid, 2013. PDF. Pages 2835.
 July 2013 Verifying the bridge between Simplicial Topology and Algebra: the EilenbergZilber algorithm, L. Lamban, F. J. MartinMateos, J. Rubio and J. L. RuizReina, PDF. Logic Journal of the IGPL. DOI link.
 July 2013: The Rooster and the Butterflies, A. Mahboubi. CICM 2013. Invited paper in the Proceedings of Conferences on Intelligent Computer Mathematics  2013, Bath 2013. PDF DOI link.
 July 2013: Canonical Structures for the working Coq user, A. Mahboubi and E. Tassi. ITP 2013. Invited paper in the proceedings of the 4th Conference on Interactive Theorem Proving, ITP 2013, Rennes, 2013. PDF DOI link.
 July 2013: A MachineChecked Proof of the Odd Order Theorem, Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi and Laurent Thery. ITP 2013. Proceedings of the 4th Conference on Interactive Theorem Proving, ITP 2013, Rennes, 2013. Pages 163179 PDF DOI link
 July 2013: Pragmatic Quotient Types in Coq, C. Cohen. ITP 2013. Proceedings of the 4th Conference on Interactive Theorem Proving, ITP 2013, Rennes, 2013 DOI link.
 July 2013: Certification of inequalities involving transcendental functions: combining SDP and maxplus approximation, X. Allamigeon and S. Gaubert and V. Magron and B. Werner. ECC'13. Proceedings of the European Control Conference, ECC'13, Zurich, 2013. PDF .
 July 2013: Certification of bounds of nonlinear functions : the templates method, X. Allamigeon and S. Gaubert and V. Magron and B. Werner. CICM 2013. Lecture Notes in Computer Science, 7961, 2013. PDF DOI link.
 July 2013: Verifying a platform for digital imaging: a multitool strategy, J. Heras, G. Mata, A. Romero, J. Rubio, and R. Sáenz. CICM 2013. Lecture Notes in Computer Science, 7961, pages 6681, 2013. PDF. Web page. DOI link.
 June 2013: Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study web page, 2013.
 June 2013: Certified Symbolic Manipulation: Bivariate Simplicial Polynomials, L. Lamban, F. J. MartinMateos, J. Rubio and J. L. RuizReina, ACM Press, pages 243250, ISSAC 2013, DOI link, PDF, 2013.
 June 2013: Spectral sequences for computing persistent homology of digital images, A. Romero, J. Heras, G. Mata, J. Rubio, F. Sergeraert, ACA 2013, Proceedings, PDF, pages 331335, 2013. ISBN10: 8461645650.
 March 2013: The Picard Algorithm for Ordinary Differential Equations in Coq, Evgeny Makarov and Bas Spitters, Rough Diamond, ITP2013 PDF, 2013 DOI link.
 February 2013: The Role of Formalization in Computational Mathematics, Julio Rubio. Bulletin Belgian Mathematical Society (BBMS), 20(3), (2013) 385403. Paper link. Preliminary PDF.
 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 SasakiMurao Algorithm, T. Coquand, A. Mörtberg and V. Siles. Journal of Formalized Reasoning, vol 5, No 1. DOI link, To PDF.
 August 2012 A RefinementBased 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 361376, 2012. DOI link PDF.
 July 2012: Verifying an algorithm computing Discrete Vector Fields for digital imaging, J. Heras, M. Poza, and J. Rubio. CICM 2012, Lecture Notes in Computer Science, 7362, pages 215229, 2012. PDF, DOI link, Arxiv link.
 May 2012: Towards a certified 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 4957, 2012. PDF, DOI link.
 March 2012: Computerassisted 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.75104. RSME 2012
 February 2012 A constructive proof of Simpson's Rule, Thierry Coquand and Bas Spitters. Logic and Analysis 4:15 pp18 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 113120, 2012. SpringerVerlag. PDF, DOI link.
 January 2012: Formalization of a Normalization Theorem in Simplicial Topology . L. Lambán, F. J. MartínMateos, J. L. RuizReina, J. Rubio. Annals of Mathematics and Artificial Intelligence 64(1), 2012, pp. 137. 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. ImageNA 2(4), 2011, pp. 2931. PDF. ImageNA 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.
 September 2011: How to make ad hoc proof automation less ad hoc. G. Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer. ICFP 2011, ICFP 2011, 163175, ACM DOI Link.
 August 2011: Pointfree, setfree concrete linear algebra. G. Gonthier. ITP 2011, Lecture Notes in Computer Science, 6898, pp. 103118. PDF. DOI Link.
 August 2011: Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials. L. Lambán, F. J. MartínMateos, J. L. RuizReina, J. Rubio. ITP'11. Lecture Notes in Computer Science, 6898, pages 200215, 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. 731761. 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. 683714. 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 3044, 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, 90106. 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 962970, 2011. Pdf. DOI link
 September 2010: An introduction to small scale reflection in Coq Georges Gonthier, Assia Mahboubi, PDF, Journal of Formalized Reasoning, vol 3, No2 DOI link.
 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. Lecture Notes in Computer Science, 6564, pages 3751, 2011. SpringerVerlag. Pdf, DOI link.
 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, DOI link.
 July 2010: Automated MachineChecked Hybrid System Safety Proofs Herman Geuvers, Dan Synek, Adam Koprowski, Eelis van der Weegen at ITP10. 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 204218, SpringerVerlag. 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
 June 2013 Java program verification for digital image processing, R. Sáenz, Degree's Thesis (text in English), PDF.
 June 2013 Certifying homological algorithms to study biomedical images, M. Poza, PhD Thesis, University of La Rioja (Spain) PDF.
 June 2013 Transforming (almost) without programming: a case of interoperability among theorem provers, J. Aransay, J. Divason, J. Heras, L. Lamban, V. Pascual, A. L. Rubio and J. Rubio, PDF.
 June 2013 Obtaining an ACL2 specification from an Isabelle/HOL theory, J. Aransay, J. Divason, J. Heras, L. Lamban, V. Pascual, A. L. Rubio and J. Rubio, PDF. Web page.
 May 2013 Sets in homotopy type theory, Egbert Rijke and Bas Spitters, ArXiV.
 May 2013 Neuron detection in stack images: a persistent homology interpretation, J. Heras, G. Mata, G. Cuesto, J. Rubio and M. Morales, PDF.
 April 2013: Computable Refinements by Quotients and Parametricity, Cyril Cohen, Maxime Dénčs, Anders Mörtberg, Abstract, TYPES2013 PDF.
 March 2013 A Hierarchy of mathematical structures in ACL2, J. Heras, F.J. MartínMateos 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 firstorder theory, C. Cohen, PhD Thesis, École Polytechnique (France) PDF
 September 2012 Constructive Algebra in Type Theory, A. Mörtberg, Licentiate Thesis, Chalmers University of Technology and University of Gothenburg (Sweden) PDF
 June 2012: Report on J. Heras stay in Göteborg, J. Heras, PDF.
 October 2011: Proofs of properties of finitedimensional vector spaces in Isabelle/HOL, J. Divasón. Degree's Thesis, PDF, 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. Pdf.
 February 2011: A certified module of Simplicial Complexes for the Kenzo system. Technical report by J. Heras, V. Pascual and J. Rubio. Pdf.
 November 2010: Formal Verification for Numerical Methods, Ioana Pasca, PhD Thesis, University of Nice Sophia Antipolis. Author version.
 August 2010: Hybrid System verication 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ínMateos, J. L. RuizReina, J. Rubio. Technical report. Pdf.
 June 2010: Report on a SSReflect week. Technical report by Yves Bertot, Laurence Rideau and ForMath La Rioja node. Pdf.
 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
 September 2013 Bas Spitters, Sets in homotopy type theory, Type Theory, Homotopy Theory and Univalent Foundations, PDF
 September 2013 Assia Mahboubi. Automated and (Formally) Certified Proofs of Summation Formulae, Humboldt Kolleg. Proof 2013. PDF.
 July 2013 Bas Spitters, Recent progress in homotopy type theory, Coq workshop, Invited lecture PDF
 June 2013 Rubén Sáenz. Java program verification for digital image processing, Universidad de La Rioja (slides in Spanish). PDF.
 June 2013 María Poza. Certifying homological algorithms to study biomedical images. PhD Thesis. Slides thesis defense.
 May 2013 Egbert Rijke and Bas Spitters, Cauchy reals in the univalent foundations, Brouwer seminar PDF.
 May 2013 Egbert Rijke and Bas Spitters, Higher inductive types, Brouwer seminar PDF.
 May 2013 Certified Global Optimization using Maxplus based Templates (Victor Magron) LAAS Seminar Slides.
 April 2013 Formal Nonlinear Optimization via Templates and SumofSquares (Victor Magron) TYPES 2013 Slides.
 April 2013 Maxime Dénčs, Cyril Cohen and Anders Mörtberg. Computable data refinements by quotients and parametricity TYPES 2013 Slides.
 January 2013 Orthogonal factorization systems in HoTT (Egbert Rijke) notes video.
 December 2012: Anders Mörtberg, Thierry Coquand, Vincent Siles. Coherent and Strongly Discrete Rings in Type Theory. CPP 2012. Slides.
 November 2012: Evgeny Makarov and Bas Spitters. Solving Ordinary Differential Equations in Coq. 2nd ForMath Juniors Meeting. Slides.
 October 2012: Julio Rubio. Algebraic Topology: formalization and applications. IV Iberian Mathematical Meeting. Slides.
 September 2012: Julio Rubio. Interdisciplinary research: mathematics, computer science and biology (in Spanish). Seminario de Actualización en Matemáticas. Slides.
 September 2012: Maxime Dénčs. Verifying computer algebra algorithms: refinements and automation to the rescue. MAP 2012. Slides.
 September 2012: Julio Rubio. Formalisation of Algebraic Topology: a report. MAP 2012. Slides.
 September 2012: Anders Mörtberg. A Formal Proof of SasakiMurao Algorithm. MAP 2012. Slides.
 August 2012: Maxime Dénčs, Anders Mörtberg and Vincent Siles A refinementbased approach to computational algebra in Coq. ITP 2012. Slides.
 August 2012: Maxime Dénčs. Experience report on computation inside Coq. Coq Workshop 2012. Slides.
 August 2012: Victor Magron, Certification of inequalities involving transcendental functions using SemiDefinite Programming. ISMP 2012. Slides.
 August 2012: Yves Bertot, What is π? Investigating the definition of π in Coq's libraries. 2012 Coq Workshop. Slides.
 June 2012: J. Aransay and J. Divasón. Formalizing an Abstract Algebra Textbook in Isabelle/HOL. XIII Encuentro de Álgebra Computacional y Aplicaciones (EACA 2012). Slides.
 June 2012: J. Heras, G. Mata, M. Poza, and J. Rubio. Symbolic Manipulation and Biomedical Images. XIII Encuentro de Álgebra Computacional y Aplicaciones (EACA 2012). Slides.
 June 2012: J. Heras, F.J. MartínMateos, and V. Pascual. An ACL2 formalization of Algebraic Structures. XIII Encuentro de Álgebra Computacional y Aplicaciones (EACA 2012). Slides.
 June 2012: J. Rubio. The Role of Formalization in Computational Mathematics. Plenary talk at 1st Joint Conference of the Belgian, Royal Spanish and Luxembourg Mathematical Societies Slides.
 May 2012: J. Heras, M. Dénčs, G. Mata, A. Mörtberg, M. Poza and V. Siles. Towards a certified computation of homology groups from biomedical images. Slides.
 March 2012: From computational analysis to thoughts about analysis in HoTT, Bas Spitters. MAP Spring School.
 March 2012: J. Heras, G. Mata and J. Rubio. Neuronal structure detection using Persistent Homology. Slides.
 March 2012: J. Rubio. Formalization of Mathematics: Why Algebraic Topology? MAP International School on Formalization of Mathematics 2012 Slides.
 January 2012: Computation of Homology groups, J. Heras, paperandpencil proof.
 December 2011: J. Rubio. Verifying software, verifying mathematics. MAP 2011 Slides.
 October 2011: J. Divasón. Proofs of properties of finitedimensional vector spaces. Thesis Defence, Slides.
 September 2011: Cyril Cohen. Quantifier elimination in real closed fields: a formal proof. Types 2011. Slides.
 September 2011: Anders Mörtberg. Rings with explicit divisibility formalized in Coq. Types 2011. Slides.
 August 2011: Maxime Dénčs, Yves Bertot. Experiments with computable matrices in the Coq system. Coq Workshop 2011. Slides.
 August 2011: L. Lambán, F.J. MartínMateos, J. Rubio, and J.L. RuizReina. Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials. ITP 2011. Slides.
 July 2011: Enrico Tassi, Features proposal: tunable simplify and SSR contextual patterns. Coq GT July 2011 Slides
 July 2011: Robbert Krebbers and Bas Spitters, Computer certiﬁed eﬃcient exact reals in Coq. Logic Colloquium, special session on Proof Theory and Constructive Mathematics, 1116 July 2011, invited lecture. Slides.
 July 2011: J. Heras, M. Poza, M. Dénčs, and L. Rideau. Incidence Simplicial Matrices formalized in Coq/SSReflect. CICM 2011. Slides.
 July 2011: A. Mahboubi. "Constructive quantifier elimination for real numbers and complex numbers, in a proof assistant". Talk at the PPS team seminar (Paris 7 University) Slides
 June 2011: J. Heras, G. Mata, M. Poza, and J. Rubio. Homological Processing of Biomedical digital images: automation and certification. ACA 2011. Slides.
 May 2011: Mathematical Knowledge Management in Algebraic Topology, Jónathan Heras, PhD Thesis, University of La Rioja. Slides thesis defense.
 March 2011: Robbert Krebbers, Bas Spitters and Eelis van der Weegen. Type Classes for Mathematics. Workshop on reification and generic tactics. Slides.
 February 2011: J. Heras, V. Pascual and J. Rubio. A certified module of Simplicial Complexes for the Kenzo system. Thirteen International Conference on Computer Aided Systems Theory. EUROCAST2011 Slides.
 November 2010: Talks at MAP 2010
 October 2010: Cyril Cohen. "Formalized foundations of polynomial real analysis". Talk at the Types 2010 workshop, Warsaw, Poland. Slides
 September 2010: J. Heras and M. Poza. Incidence Matrices of Simplicial Complex in SSreflect. Stay in the Sophia Antipolis node of INRIA. Slides.
 September 2010: Jesús Aransay, Julio Rubio and Clemens Ballarin, Generating certified code from formal proofs: a case study in Homological Agebra. PROLE2010. Slides
 July 2010: J. Heras, V. Pascual and J. Rubio. Proving with ACL2 the correctness of simplicial sets in the Kenzo system. 20th International Symposium on LogicBased Program Synthesis and Transformation LOPSTR 2010. Slides.
 July 2010: Y.Bertot, F. Guilhot, and A. Mahboubi. Root Isolation for onevariable polynomials. Coq Workshop 2010. Slides.
 July 2010: C. Cohen and A. Mahboubi. A formal quantifier elimination for algebraically closed fields. 17th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning. Calculemus 2010. Slides.
 May 2010: J. Rubio. Mechanising mathematics: the case of Algebraic Topology. Invited talk at the Conference in honor of Tomas Recio. Slides.
 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. Slides.
 April 2010: J. Aransay. Living (i.e. executing and proving) with different representations of datatypes. Workshop on Algebraic computing, soft computing, and program verification. Slides.
 April 2010: C. Dominguez. Combining formalization and computation in Coq: a casestudy with algebraic structures. Workshop on Algebraic computing, soft computing, and program verification. Slides.
