Course Syllabus
Following is the list of topics that we intend to cover in the course. We hope that at the end of the course, students will be able to do research in this area.
- Starting Lean
- A quick tour with examples
- Dependent data types
- Simple type theory and examples of higher types
- Dependent Pi’s and Sigma’s
- Notions of reduction
- Implicit arguments
- Type theory as a proof language (Curry-Howard)
- Propositional logic in type theory
- Quantifiers and quantifiers rules
- Equality rules and calculational proofs
- Aside: constructive logic vs. classical logic
- Lean’s user interface (emacs) - a guided tour
- Printing options
- Searching
- Building longer proofs
- Tactics and the tactic frameworks
- Structured proofs
- Sections and contexts
- Inductive types
- Examples: nat, list, tree
- Proofs by induction, definitions by recursion
- Inductive definitions of equality, and, or, false, true, unit, empty
- Inductive families, parameters vs. indices
- The simplifier
- Term rewriting
- Setoids
- Struggling with dependent types
- Sigma types and equality of dependent pairs
- eq.rec, casts, and heterogeneous equality
- intensional vs. extensional type theory
- Structures and type classes
- Encodings of type classes
- Representing structures like orders and groups
- Classical logic and other axioms
- EM with type classes
- Function extensionality
- Skolem functions
- Programming language semantics in type theory
- Lean’s parser
- Pratt-style parsing
- Declaring notation
- Homotopy type theory
- Overview and introduction
- The elaborator
- Higher-order unification
- Overloading
- An overview of Lean’s elaboration algorithm
(Later: using other automated tools)