# Calendar

## Past topics

## Final project work

- Apr 18
- Day 1
- Apr 20
- Day 2

## Logical foundations of Lean

- Apr 6
- Type universes and the oddball Prop
- Sections 12.1-12.3

- Apr 11
- Subtypes
- Section 12.4

- Apr 13
- Quotient types
- Section 12.5

## Verification, Specification, and Inductive Predicates

- Mar 14
- An inductive predicate for sorted lists
- Chapter 6

- Mar 16
- Insert sort in Lean
- Mar 21
- Prove that our InserSort sorts
- Mar 23
- Refactor from Bool to Decidable Prop
- Mar 28
- Compiling and running Lean code

## Interlude

- Mar 2
- Advent of Code
- 2022 Day 1

## Programming constructs in Lean

- Feb 16
- Structures
- Section 5.5

**Quiz 5**- Feb 21
- More on structures
- Feb 23
- Classes and instances
- Section 5.6

**Quiz 6**- Feb 28
- Categories via classes
- Mar 30
- Monads
- Chapter 7

- Apr 4
- Monads II: the re-monading

## Proofs and tactics

- Jan 24
- Theorems and proofs
- Sections 2.3-3.1

**HW 1 due**- Jan 26
- First tactics and some logic
- Sections 3.2-3.3

**Quiz 2**- Jan 31
- Quantifiers in Lean
- Sections 3.3

**HW 2 due**- Feb 2
- More quantifiers and equality in Lean
- Sections 3.4-3.5

**Quiz 3**- Feb 7
- Induction in Lean
- Section 3.6

**HW 3 due**- Feb 9
- More tactics
- Sections 4.1-4.2

**Quiz 4**- Feb 14
- Calc tactic & proof terms
- Sections 4.3-4.4

**HW 4 due**

## Terms, types, and type-checking

- Jan 12
- Terms and types
- Sections 1.1-1.2

- Jan 17
- Type checking and type inhabitation
- Sections 1.3-1.4

- Jan 19
- Intro to inductive types
- Sections 2.1-2.2

**Quiz 1**

## Introduction and setup

- Jan 10
- Orientation

About this webpage. Copyright © 2023 Matthew Ballard. Distributed with an MIT license.