2 Outline

This outline is correct in terms of topics and ordering. It’s customary to give timings, but for my courses, those numbers are fictitious anyway, since I don’t prepare each lecture as a clearly-defined unit. Each of the three sections should take about one-third of the time we have.

1. Introduction and Propositional logic

Overview and motivation. Formulas. The Boolean interpretation. Proof for the implicational fragment. Proofs as programs. Proust for implication. Adding the other connectives. Classical vs intuitionistic logic.

2. Predicate logic

Classical first-order logic. Refactoring Proust for implication. Universal quantification in higher-order logic. Debugging the implementation. Equality and arithmetic. Existential quantification in higher-order logic.

3. Proof assistants

Common features of Agda and Coq. Agda, starting from nothing. Logic. Ordering. Equality. Natural numbers. Sorting. Data structures. (Optional readings and exercises using Coq.)