Course | Fundamentals of Dependent Types

Learn a wide range of techniques dependent types, giving you a sneak peak of the future of programming languages!



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
  • Implicits

  • Dependent types in a non-dependent language
  • Afternoon session: proving properties about your code

    • The Equality type
    • Stating theorems, and proving by coding
    • Properties as data types
    • Intrinsic vs. extrinsic verification

    Company and Private Group Training

    Company and Private Group Training


    • Dependent Types
    • Agda
    • Coq
    • Arend
    • Theorem Proving
    • Haskell

    This Fundamentals of Dependent Types includes:

    • Maximum Class Size of 15
    • Access to Academy EduTools Platform
    • Access to Course Materials
    • Certificate of Completion
    • Access to a Private Channel with Trainers in the Academy Slack
    • A Q&A session one week post-course
    • A pre-and-post meeting with our trainers