This course, Programming Languages, is about the theory for the following questions: is this program correct? why is it correct? why is it not correct? how to describe the behavior of a program? how to describe the designed functionality of a program? You will learn operational semantics, denotational semantics, Hoare logic and basic functional programming and proof engineering in Coq.