ForMath /

Papers and Slides

Table of contents:

Publications in Journals, Conferences and Workshops
Thesis, Technical Reports and Preprints
Slides

Publications in Journals, Conferences and Workshops

September 2014: 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. AISC 2014. Lecture Notes in Artificial Intelligence, 8884, 2014. PDF. Web page.
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 28--35.
July 2013 Verifying the bridge between Simplicial Topology and Algebra: the Eilenberg-Zilber algorithm, L. Lamban, F. J. Martin-Mateos, J. Rubio and J. L. Ruiz-Reina, 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 Machine-Checked 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 163--179 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 max-plus 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 non-linear 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 multi-tool strategy, J. Heras, G. Mata, A. Romero, J. Rubio, and R. Sáenz. CICM 2013. Lecture Notes in Computer Science, 7961, pages 66--81, 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. Martin-Mateos, J. Rubio and J. L. Ruiz-Reina, ACM Press, pages 243-250, 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 331--335, 2013. ISBN-10: 84-616-4565-0.
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) 385--403. 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 Sasaki-Murao Algorithm, T. Coquand, A. Mörtberg and V. Siles. Journal of Formalized Reasoning, vol 5, No 1. DOI link, 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. CICM 2012, Lecture Notes in Computer Science, 7362, pages 215--229, 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 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.
September 2011: How to make ad hoc proof automation less ad hoc. G. Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer. ICFP 2011, ICFP 2011, 163-175, ACM 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. 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 37--51, 2011. Springer-Verlag. Pdf, DOI link.
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

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.
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í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
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 finite-dimensional 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ín-Mateos, J. L. Ruiz-Reina, 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 Sum-of-Squares (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 Sasaki-Murao Algorithm. MAP 2012. Slides.
August 2012: Maxime Dénès, Anders Mörtberg and Vincent Siles A refinement-based 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 Semi-Definite 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ín-Mateos, 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, paper-and-pencil proof.
December 2011: J. Rubio. Verifying software, verifying mathematics. MAP 2011 Slides.
October 2011: J. Divasón. Proofs of properties of finite-dimensional 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ín-Mateos, J. Rubio, and J.L. Ruiz-Reina. 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, 11-16 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
- Assia Mahboubi. Cylindrical Algebraic Decomposition in Coq. A four lecture tutorial: Part 1, Part 2, Part 3, Part 4.
- Bas Spitters: Towards Numerical Integration in Coq
- Jónathan Heras: Formal Libraries for Algebraic Topology: Status Report
- Anders Mörtberg: Constructive Algebra in Functional Programming and Type Theory
- Maxime Dénès: Experiments towards Efficient Computations in Formalised Linear Algebra
- Georges Gonthier: Formalising the Structure of Extremal p-groups
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 Logic-Based Program Synthesis and Transformation LOPSTR 2010. Slides.
July 2010: Y.Bertot, F. Guilhot, and A. Mahboubi. Root Isolation for one-variable 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 case-study with algebraic structures. Workshop on Algebraic computing, soft computing, and program verification. Slides.