This course presents principles and techniques of programming, focusing on sophisticated methods for specifying, constructing, and reasoning about computer programs. Via features of a high-level functional programming language (currently ML), this course concretely illustrates mechanisms for building user-defined data types, including recursive and polymorphic types, and infinite data structures such as streams; for building higher-order control constructs such as first-class functions and continuations; and for building large programs using advanced module composition. It also introduces the use of formal methods for specifying and verifying programs.