2009 , Volume 14, № 1, p.3-6

The purpose of this article is to discuss my research of Martin-Loеf's type theory. It consists of a number of scholastic proofs and results. In order to use a theory it is a requirement to prove its consistency. One of my results is a proof of consistency of Martin- Loеf's type theory. It has been submitted for publication in “Springer Archive for Mathematical Logic”'. Another problem is the efficiency of the generated computer programs. This problem can be reformulated into a problem of comparison of complexity of inferences in the type theory and in other known systems, in the Hilbert-type System, and in the Gentzen-type System.
I will present an overview of my algorithm that automates the construction of an object of the type that represents the problem under question. The construction of this algorithm raises fixed-point type problems. I presented my algorithm in 1986 at the “Personal Computers & Local Networks” conference in Georgia.