Type theory, computer algebra & dynamical systems

Type theory is one of most active directions in modern mathematical logic. It supports constructive formatlization of mathematical computations, including analytical ones. Type theory is used as basis in most of so called proof assistants (software supporting interactive proof-check and development). One of important problems is the problem of efficient combined use of proof assistants and computer algebra systems. Here this problem is considered in the context of complex multiparametric nonlinear dynamical systems represented by differential equations of some types. The work has been done at partial financial support of the grant, N 01-05 of the French-Russian Lyapunov Center.