Reseña: Construction of real algebraic numbers in Coq
El lunes (13 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Coq titulado Construction of real algebraic numbers in Coq.
Su autor es Cyril Cohen (de la École Polytechnique (Palaiseau, Francia)).
El resumen del trabajo es
This paper shows a construction in Coq of the set of real algebraic numbers, together with a formal proof that this set has a structure of discrete archimedian real closed field. This construction hence implements an interface of real closed field. Instances of such an interface immediately enjoy quantifier elimination thanks to a previous work. This work also intends to be a basis for the construction of complex algebraic numbers and to be a reference implementation for the certification of numerous algorithms relying on algebraic numbers in computer algebra.
El código de la formalización en Coq se encuentra en realalg.tgz.