Principles of Functional Programming
Course ID 15150
Description An introduction to programming based on a "functional" model of computation. The functional model is a natural generalization of algebra in which programs are formulas that describe the output of a computation in terms of its inputs---that is, as a function. But instead of being confined to real- or complex-valued functions, the functional model extends the algebraic view to a very rich class of data types, including not only aggregates built up from other types, but also functions themselves as values. This course is an introduction to programming that is focused on the central concepts of function and type. One major theme is the interplay between inductive types, which are built up incrementally; recursive functions, which compute over inductive types by decomposition; and proof by structural induction, which is used to prove the correctness and time complexity of a recursive function. Another major theme is the role of types in structuring large programs into separate modules, and the integration of imperative programming through the introduction of data types whose values may be altered during computation. NOTE: students must achieve a C or better in order to use this course to satisfy the pre-requisite for any subsequent Computer Science course.
Key Topics
Recursion; Specifications and Correctness Proofs; Work and Span Analysis; Parallelism; Polymorphism; Higher-order Functions; Modular Programming
Learning Resources
Lecture Notes by the course instructors; Piazza forum for Q&A and discussions; git to distribute homeworks; There are also well-known textbooks on introduction to functional programming in ML for those who seek additional resources.
Course Relevance
Intro level course to functional programming.
Course Goals
Write well-typed functional programs using the language ML; Develop specifications and prove program correctness using rigorous techniques; Apply equational, evaluational, and compositional reasoning techniques, and use mathematical and structural induction in proofs; Analyze sequential and parallel running time of programs using the concepts of work and span; Develop cost graphs and recurrences from programs, and use them to derive asymptotic bounds on work and span; Use abstract types and modules to structure code with clear and well-designed interfaces
Identify opportunities for parallelism in code and exploit parallelism by choosing appropriate data structures and function designs
Pre-required Knowledge
Basic mathematical background such as ability to do proof by induction, and familiarity with the core mathematical structures of Computer Science, such as sets, relations, graphs, and trees.
Assessment Structure
Homework (35%); Labs (10%); Midterms (30%); Final (25%)
Course Link
http://www.cs.cmu.edu/~15150/