This course will introduce students to type theory and thus to the integration of logic and functional programming. Students will learn to use the Coq proof assistant. Topics to be covered include inductive data type definitions, pure functional programming, propositions as types, logical representation of properties and relations, proof engineering, programs as data, program evaluation, Hoare Logic, lambda calculus, and type checking.