Warning 1.1.
The instructor reserves the right to modify the schedule as needed.
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
