ALGEBRAIC POWER SERIES: REPRESENTATION AND EFFECTIVENESS OF DIVISION
In the talk we give an approach to some topics of Computational Algebra as standard bases computation and canonical forms in the setting of algebraic power series. 
POLYNOMIAL ALGEBRA BY VALUES This talk outlines some new algorithms for operations on multivariate polynomials. The point of view taken in the talk is a dual viewpoint, namely that all polynomials considered are given by their values at known points, and that the degrees of the polynomials are known or can be deduced. The first nontrivial algorithm considered is division; then Bezout matrices, generalized companion matricies, GCD, and the solution of zerodimensional polynomial systems are investigated. A new algorithm is given for such solution: neither Gröbner basis nor resultantbased, it shares some characteristics with resultant algorithms. A preprint of a paper detailing this talk can be found at http://www.orcca.on.ca/TechReports/2004/TR0401.html. This is joint work with Laureano GonzalezVega, Amir Amiraslani, and Azar Shakoori. 
CLASSIFYING SERIAL MANIPULATORS:
COMPUTER ALGEBRA AND GEOMETRIC INSIGHT. This talk is intended to present the work of a group including researchers in robotics, computer algebra and geometry and studying the possible behaviours of a simple manipulator when one varies the design parameters (length of arms, offset). One important aspect of this behaviour is the ability to change posture without crossing singularities. The output of the work is a partition of the space of parameters into cells where the behaviour remains the same. We plan to emphasize the interplay between the algebraic modelisation of the problem, the use of specialized computer algebra tools and the geometric analysis of occurring phenomena. 
IMPLICITATION AND COMMUTATIVE ALGEBRA
The talk would discuss implicitization using A) resultants and B) moving surfaces and C) relations between the two. The talk would illustrate how concrete questions in implicitization leads naturally to concepts in commutative algebra such as syzygies, free resolutions, regularity, and local complete intersections. The talk would be downtoearth but the moral would be that serious commutative algebra is involved. There would be lots of examples. 
COMPUTATIONAL ASPECTS OF MOVING FRAMES
In this talk, I will describe a new approach to the powerful Cartan theory of moving frames. The method is completely algorithmic, and applies to very general Lie group actions. I hope to discuss a wide variety of new applications, including classification of differential invariants, geometrical equivalence of curves and surfaces, symmetries of polynomials in classical invariant theory, object recognition in computer vision, invariant variational problems, and the design of symmetrypreserving numerical approximations. the emphasis will be on computer algebra aspects of the methods. 
VERIFICACION FORMAL Y SISTEMAS DE CALCULO SIMBOLICO Verificar formalmente un programa significa demostrar, usando una lógica formal, que el programa cumple con las propiedades de corrección que se esperan del mismo, expresando igualmente estas propiedades en la misma lógica. Nuestra confianza en los cálculos realizados por un programa se verá incrementada sustancialmente si éste ha sido formalmente verificado. Usualmente, esta verificación formal se lleva a cabo con la ayuda de algún sistema de demostración automática de teoremas. En esta conferencia, pretendemos explicar técnicas que pueden ser aplicadas a la verificación formal de algoritmos implementados en sistemas de cálculo simbólico. En este caso, además del esfuerzo de verificación usual que se necesita para demostrar la corrección de cualquier proceso computacional, debemos formalizar también toda la rica y extensa teoría matemática necesaria para poder expresar las propiedades de corrección de los programas. En particular, describiremos nuestra experiencia con el demostrador de teoremas ACL2, usado para implementar y verificar algunos algoritmos bien conocidos presentes en la mayoría de los sistemas de cálculo simbólico. FORMAL VERIFICATION AND SYMBOLIC COMPUTATION SYSTEMS Formal verification of a program means the act of proving, using a formal logic, that the program meets its intended correctness properties, formally expressed in the same logic. Our confidence in the results computed by a program increases if it is formally verified. Usually, this formal verification is carried out with the assistance of a mechanized reasoning system. In this talk, we intend to explain how we can formally verify some algorithms typically implemented in symbolic computation systems. In this case, in addition to the usual verification effort needed to prove correctness properties of the computation processes implemented, we must formalize also all the (usually rich) mathematical theory needed to express the properties of the program. In particular, we show our experience with the use of the ACL2 mechanized reasonig system for the implementation and verification of some wellknown algorithms present in most of symbolic computation systems. 
CERTIFYING COMPUTER ALGEBRA PROGRAMS,
DATA SAFETYIN THE FoC LANGUAGE The talk presents the main features of the FoC programming environment and its basic notions. Going through the example of an implementation of distributed and recursive polynomials we introduce some FoC concepts. FoC's species and collections allow to give a mathematical view of FoC types and values of a type are safely interpreteds as mahematical objects. We will present the static analysis performed in FoC and show that data type safety can be achieved. 
