[JadeNB]

Another thread https://news.ycombinator.com/item?id=22783645 recommended Verified Functional Programming in Agda (https://dl.acm.org/doi/book/10.1145/2841316). I was just thrilled to notice that the HOPL proceedings (https://dl.acm.org/conference/hopl) are there!

EDIT 1: HOPL was pointed out earlier by spdegabrielle (https://news.ycombinator.com/item?id=22795488).

EDIT 2: I was just downloading, and got my IP address blocked. Nothing crazy or automated, just manually clicking through to all the articles in HOPLs I–III. Hopefully it'll clear up eventually, but just a warning to anyone else trying to build a library in a day.