Just this morning these two books landed my mailbox:
The Little Typer is a new book on dependent type theory, written by Daniel P. Friedman, an author of The Little Schemer, and David Thrane Christiansen, an Idris contributor. Verified Functional Programming in Agda is a book by Aaron Stump, on using dependent types in Agda to prove various properties of programs. After having read the Type-driven Development with Idris book by Edwin Brady, I am hoping these two books will significantly expand my knowledge of and improve my skills in type theory, theorem proving and typed functional programming. Looking forward to reading the books! If you haven’t noticed by now, I got hooked on dependent types!