Type theory, computer algebra, proof assistants and grammars

This article provides a brief overview and review of the main areas of research related to type theory and their applications. A description of universal systems of analytical calculations (Computer Algebra), as well as support systems of analytical calculations (Proof Assistants) are given. The application types in Computer Science, above all, functional and object-oriented programming has been discussed. Specialized the main research teams which are working out research and development of software systems in this area.