In which I discover why the domino analogy for explaining induction always bothered me!

We consider the basic idea of the Curry-Howard isomorphism, that constructive proofs are essentially programs, and vice versa.  Several simple examples.  Why the law of excluded middle is not a legal constructive proof.

The basic idea of the Curry-Howard isomorphism, and its connection to the contents of Chapters 1 and 2.  Constructive proof.  A famous nonconstructive proof.

More about the structured recusion scheme known as the catamorphism.  Basic idea of functors.

Review of basic application of category theory for functional programming.  Recursion schemes are combinators that let you write point-free recursions.

A few very basic ideas of categories and combinators.  Also, the problem of understanding very concise code.

Relation of point-free functional programming to category theory.

Higher-order functions help make it possible to program in a point-free style, where we use combinators to connect functions, rather than calling the functions on inputs explicitly.  

Discussion of datatypes for tree-like data structures in functional languages.  Usefulness of these for processing structured linguistic artifacts, where the structure is represented by the tree structure.

Start of discussion of some of technology and culture that lead to more concise code in functional programming languages.  Type inference to avoid writing types for local and input variables.  Some basics of static and dynamic typing.