6.8

2 Outline

This outline is correct in terms of topics and ordering. The times are largely guesses and may not be accurate. We’ll just start the material and see how it goes.

1. Introduction (1.5 hours)

2. Propositional logic (12 hours)

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

3. Predicate logic (15 hours)

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.

4. Proof assistants (7.5 hours)

An overview. Coq from scratch in lectures (Agda in tutorials). Cool examples as time permits.