In this lecture, we study Curry-Howard correspondence and Intuitionistic implicational logic (IIL).