Skip to main content
Logo image

Section 1 Schedule

Subsection 1.1 March 12 – March 14

Introduction and Setup

Subsection 1.2 March 17 – March 21

  • 1 Types and Terms
    • 1.1 Types
    • 1.2 Terms
    • 1.3 Type Checking and Type Inference
    • 1.4 Type Inhabitation

Subsection 1.3 March 24 – March 28

  • 2 Programs and Theorems
    • 2.1 Type Definitions
    • 2.2 Function Definitions
    • 2.3 Theorem Statements

Subsection 1.4 March 31 – April 4

  • 3 Backward Proofs
    • 3.1 Tactic Mode
    • 3.2 Basic Tactics
    • 3.3 Reasoning about Connectives and Quantifiers

Subsection 1.5 April 7 – April 11

  • 3 Backward Proofs
    • 3.4 Reasoning about Equality
    • 3.5 Rewriting Tactics
    • 3.6 Proofs by Mathematical Induction
    • 3.7 Induction Tactic

Subsection 1.6 April 14 – April 18

  • 4 Forward Proofs
    • 4.1 Structured Proofs
    • 4.2 Structured Constructs
    • 4.3 Forward Reasoning about Connectives and Quantifiers
    • 4.4 Calculational Proofs

Subsection 1.7 April 21 – April 25

  • 5 Functional Programming
    • 5.5 Structures

Subsection 1.8 April 28– May 2

  • 5 Functional Programming
    • 5.6 Type Classes

Subsection 1.9 May 5 – May 9

  • 7 Effectful Programming
    • 7.1 Introductory Example
    • 7.2 Two Operations and Three Laws
    • 7.3 A Type Class

Subsection 1.10 May 12– May 16

  • 12 Logical Foundations of Mathematics
    • 12.1 Universes
    • 12.2 The Peculiarities of Prop
    • 12.3 The Axiom of Choice

Subsection 1.11 May 19– May 23

  • 12 Logical Foundations of Mathematics
    • 12.4 Subtypes
    • 12.5 Quotient Types

Warning 1.1.

The instructor reserves the right to modify the schedule as needed.