#877 overall
Dependent Types in Agda
University of Waterloo
1 recommender · 1 thread · recommended in 1 year, 2020 · score 0.7
A short course on dependent types taught in Agda, the dependently typed functional language. It is part of Peter Ragde's Flaneries series of short courses from the University of Waterloo.
One commenter suggests it as the next step after a small Racket book, for learning dependent types once basic functional programming is understood.
Programming Languagesadvancedfreeself-paced text#agda#dependent types#functional programming#proof assistant#ragde
Recommendations by year
20062026
https://cs.uwaterloo.ca/~plragde/flaneries/ the 'teach yourself racket' small book covers Hof, Lambdas, pattern matching, then you can take his other short course on Agda to learn dependent types.
Or try ocaml https://www.cs.cornell.edu/courses/cs3110/2020sp/textbook/