Possibly the most mainstream of the dependently-typed languages, which isn’t saying much. Actually aims at being a programming language rather than a theorem prover.

• Home page
• Crash course

TODO List:

• Go through the crash course
• Get an understanding of the value proposition.