This course provides a thorough introduction to modern constructive logic, its roots in philosophy, its numerous applications in computer science, and its mathematical properties. The core topics of this course are intuitionistic logic, natural deduction, Curry-Howard isomorphism, propositions as types, proofs as programs, formulas as programs, functional programming, logic programming, Heyting arithmetic and primitive recursion, cut elimination, connections between classical and constructive logic, inductive definitions, sequent calculus, and decidable classes. Advanced topics may include type theory, proof search, linear logic, temporal logic, modal logic.