1 Introduction

      1.1 Required background

      1.2 Prospective audience

      1.3 Design philosophy

      1.4 The motivations for proof

      1.5 Informal proof in mathematics

      1.6 Informal proof in computer science

      1.7 What next?

    2 Propositional Logic

      2.1 Formulas

      2.2 The Boolean interpretation

      2.3 Proof for the implicational fragment

      2.4 Proofs as programs

      2.5 Proust for implication

      2.6 Assistance with proofs

      2.7 Adding the other connectives

      2.8 Classical vs intuitionistic logic

      2.9 Semantics for intuitionistic propositional logic

      2.10 Summary of rules for intuitionistic propositional logic

    3 Predicate Logic

      3.1 First-order logic

      3.2 Higher-order logic

        3.2.1 Rules for universal quantification

        3.2.2 Substitution and computation

        3.2.3 Implementing computation

        3.2.4 Back to predicate logic

        3.2.5 Adding definitions

        3.2.6 Simulating other features

        3.2.7 Neither proof nor assistant

        3.2.8 Equality, Booleans, and arithmetic

        3.2.9 Existential quantification

        3.2.10 Summary of rules for intuitionistic predicate logic

    4 Proof Assistants

      4.1 Common features

      4.2 Agda

        4.2.1 Up from nothing

        4.2.2 Propositional and predicate logic

        4.2.3 Ordering

        4.2.4 Equality

        4.2.5 Natural numbers

        4.2.6 Sorting

        4.2.7 Data Structures

      4.3 Coq

        4.3.1 Booleans

        4.3.2 Logic

        4.3.3 Numbers

        4.3.4 Inductively defined propositions

        4.3.5 Case study: sorting

    5 Interaction In Predicate Logic

      5.1 De Bruijn indices

      5.2 A calculus of holes

      5.3 Hiding the calculus

      5.4 Unification

    6 Handouts

    7 Resources

      7.1 Acknowledgements