Learn a wide range of techniques we can use with dependent types and get a sneak peak of the future of programming languages! This course includes indexed types, blurred term/type distinctions, use of typed holes, dependent pattern matching, and Pi and Sigma types, among others.
- Experience with Functional Programming and familiarity with the syntax of Haskell or ML.
What you'll learn
Theorem proving, including stating properties of your code and writing proofs, is also covered in-depth in the course. If time allows, we'll have a sneak peek at the exciting new world opened by Homotopy Type Theory.
The course uses Arend as language, but the concepts should be readily portable to Agda, Coq, and even advanced Haskell.
Morning session: blurring the distinction between terms and types
- Indexed types
- Powerful pattern matching
- Dependent pairs and functions
Afternoon session: proving properties about your code
- The Equality type
- Stating theorems, and proving by coding
- Properties as data types
- Intrinsic vs. extrinsic verification