Programming Language Foundations in Agda
It is written as a literate script in Agda, and available at the above URLs. The books has so far been used for teaching at the Universities of Edinburgh and Vermont, and at Google Seattle. Please send your comments and pull requests!
The book was presented in a paper (of the same title) at the XXI Brazilian Symposium on Formal Methods, 28--30 Nov 2018, and is available here:
The paper won the SBMF 2018 Best Paper Award, 1st Place.