The aim of our paper is to present the Constructive Type Theory (CTT) and some related concepts for the Swedish logicianPer Martin Löf, who constructed a formal logic system in orderto establish a philosophical foundation of constructive mathematics. He tried to overcome the deficiencies of the various theoriesconstructed to solve a problematic of set theory which is: Doesthe class of all classes is a member to itself or not? among themRussell’s Type Theory, which is founded on the concept oftype, despite its imperfections and criticisms, opened the wayto others theories like the Alonzo Church’s one which is basedon function not on set, and built what we call Lambda Calculus in1930. These theories were the origin of Constructive Type theoryand its basic concepts: type, proposition, judgment, proof…etc.