Skip to main content\(
\newcommand{\lt}{<}
\newcommand{\gt}{>}
\newcommand{\amp}{&}
\definecolor{fillinmathshade}{gray}{0.9}
\newcommand{\fillinmath}[1]{\mathchoice{\colorbox{fillinmathshade}{$\displaystyle \phantom{\,#1\,}$}}{\colorbox{fillinmathshade}{$\textstyle \phantom{\,#1\,}$}}{\colorbox{fillinmathshade}{$\scriptstyle \phantom{\,#1\,}$}}{\colorbox{fillinmathshade}{$\scriptscriptstyle\phantom{\,#1\,}$}}}
\)
Section 6 Schedule
Subsection 6.1 March 12 – March 14
- March 12
- March 14
Terms and Types
-
-
Hitchhiker’s Guide to Logical Verification, §1.1, § 1.2
Subsection 6.2 March 17 – March 21
- March 17
Definitions, Variables, Sections, Namespaces
- March 19
Logic, Structured Proofs
-
-
Hitchhiker’s Guide to Logical Verification, §4.1, §4.2
- March 21
Classical Logic
-
-
Hitchhiker’s Guide to Logical Verification, §4.1, §4.2
Subsection 6.3 March 24 – March 28
- March 24
Universal Quantifiers
-
-
Hitchhiker’s Guide to Logical Verification, §4.3
- March 26
Existential Quantifiers
-
-
Hitchhiker’s Guide to Logical Verification, §4.3
- March 28
Tactics
-
-
Hitchhiker’s Guide to Logical Verification, §3.1 – 3.8
Subsection 6.4 March 31 – April 4
- March 31
Basic Inductive Types
-
-
Hitchhiker’s Guide to Logical Verification, §5.1 – §5.4
- April 2
Constructing the Natural Numbers
- April 4
Lists
-
-
Hitchhiker’s Guide to Logical Verification, §5.1 – §5.4
Subsection 6.5 April 7 – April 11
- April 7
-
Structures
-
-
Hitchhiker’s Guide to Logical Verification, §5.5
-
Type Classes
-
-
Hitchhiker’s Guide to Logical Verification, §5.6
- April 9
- April 11
Subsection 6.6 April 14 – April 18
- April 14
- April 16
- April 18
No Classes (University Closed for Easter)
Subsection 6.7 April 21 – April 25
- April 21
No Classes (University Closed for Easter)
- April 23
- April 23
Algebraic Structures in Lean I (Operations and Monoids)
Subsection 6.8 April 28– May 2
- April 28
Class Cancelled (Jury Duty)
- April 31
Algebraic Structures in Lean II (Groups)
- May 2
Subsection 6.9 May 5 – May 9
- May 5
Algebraic Structures in Lean II (Rings and Fields)
- May 7
Morphisms (Monoids and Groups)
- May 9
Subsection 6.10 May 12– May 16
- May 12
Final Project Working Session
- May 14
Final Project Working Session
- May 16
Final Project Working Session
Subsection 6.11 May 19
- May 19
Final Project Presentation
