This course introduces Coq as a functional programming language and as a proof assistant. Some basic concepts and techniques in programming languages and their formal logical underpinnings are also introduced. They will be specified and relevant properties formally verified in Coq. The topics include operational techniques for defining language features, type systems, type safety properties, polymorphism and subtyping.