This course provides an introduction to logic and some of its important uses in computer science. The course will introduce these topics through hands-on use of a constructive logic proof assistant, in this case, Coq. Because functional programming is essential for the use of such tools, and because this paradigm greatly eases the application of mathematical logic to reasoning about software, students will be introduced to a modern functional language, namely Haskell. Topics to be covered include inductive data type definitions, pure functional programs, constructive logic, type theory, natural deduction, and propositions as types and the Curry-Howard isomorphism.