FWIW I have recently written a library that performs certified root continuation of bivariate polynomials. It makes extensive use of MPFR, and plan to include it as a Sage package. So, since the goal is to make certified computations, it would be really nice to have a formal proof of the underlying libraries.
El miércoles, 3 de mayo de 2017, 15:50:36 (UTC+2), William escribió: > > Request from Paul Zimmerman: > > "Dear William, > > I am preparing a project on the formal proof of some of the MPFR routines. > To help me convince the people that will approve this project, I'd like to > get feedback from MPFR users that a formal proof is important for them. > > Sage is one of the main users of MPFR. Please could you ask to the > main developers > of Sage if they care (or not) about a formal proof of the MPFR routines? > If they > care, please could they send me a short explanation that I could include > in my > project? > > Thank you, > Paul" > > Please email him at paul.zi...@inria.fr <javascript:> > -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To post to this group, send email to sage-devel@googlegroups.com. Visit this group at https://groups.google.com/group/sage-devel. For more options, visit https://groups.google.com/d/optout.
