Logical-Applicative Computing Based on Type Theory

The actual task of developing tools to support computational thinking is considered. Homotopy type theory is studied as a formal basis for providing computational thinking. The basic objects of the applicative environment are constructed, and considerable attention is paid to the technological means of their use. The application operation (application of a function to an argument) is considered as the main means of use, and the correctness of the application is ensured by typing the objects involved in the application. A method of parameterization of objects is considered, which allows to introduce into consideration families of objects of various types that behave similarly during application. The resulting sets of objects make it possible to define operators immersed in the basic computing environment.