CH can be applied to classical logic, too.  The seminal paper is A Formulae-as-Types Notion of Control by Timothy Griffin.  I discuss how backtracking implements the law of excluded middle.

Dependent types are discussed, particularly as used for expressing pre- and post-conditions of functions.

I follow up on some comments I made about Curry-Howard for first-order quantifiers in the previous episode.  Sheard's Omega language also mentioned (see links on his web page).  First-order quantifications turn into indexed types where the indices are not program expressions but come from another syntactic domain.

Discussion of the Curry-Howard isomorphism for the connectives of propositional logic (AND, OR, NOT, FALSE, IMPLIES).  Initial consideration of Curry-Howard for first-order and higher-order logic.  Dependent types.

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.