by Ulf Norell, Chalmers University of Technology, Sweden
Verified Functional Programming in Agda is an excellent introduction to the field of dependently typed programming. Stump does a great job of making the subject accessible to beginners without shying away from the more advanced topics.