Formal methods are of the fundamental importance for computer scientists, and this PhD-level course aims to provide a modern and up-to-date introduction to a specific subfield of formal methods: correct and secure compilation. In particular, the goals of this course are: introduce students to the syntax and semantics of programming languages in Coq (a proof assistant); familiarize students with the principles and motivations of correct and secure compilation; teach students how to use the Coq proof assistant to support mechanical proofs of compiler correctness/security. The last few hours of the course will be dedicated to more advanced topics, such as modern proof techniques or state-of-the-art applications.