A formal study of Bernstein coefficients and polynomials

DOI10.1017/S0960129511000090zbMath1236.33016MaRDI QIDQ3094174

Yves Bertot, Assia Mahboubi, Frédérique Guilhot

Publication date: 21 October 2011

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

de Casteljau algorithmBernstein coefficientsreal roots of polynomials

Mathematics Subject Classification ID

Related Items (3)

View of Computer Algebra Data from Coq ⋮ Formalization of Bernstein polynomials and applications to global optimization ⋮ Theorem of three circles in Coq

Uses Software

• Coq
• METAFONT
• C-CoRN
• ISOLATE
• Coq/SSReflect

Cites Work

• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Efficient isolation of polynomial's real roots.
• Formal proofs for theoretical properties of Newton's method
• Implementing the cylindrical algebraic decomposition within the Coq system
• A monadic, functional implementation of real numbers
• A Modular Formalisation of Finite Group Theory
• A Short Presentation of Coq
• Certified Exact Transcendental Real Number Computation in Coq
• Algorithms in real algebraic geometry

This page was built for publication: A formal study of Bernstein coefficients and polynomials