I like Conor McBride's writing style. But a lot of the files are stuff I want to look at someday but don't have time to read or need more background before reading. I need to sort them out in Zotero, they aren't curated.

One thing that I did discover is that PhD theses are a great resource. They tend to have more exposition of background information - perhaps because they're intended for a wider audience. Papers often assume you've been working in the field for a while and will assume you're already familiar with notation, terms, and results from the field.

I'm reading through Jesper Cockx' thesis, because I'm interested in how pattern matching is translated to eliminators, and Sebastian Ulrich's thesis, because I want to know how Lean4 works. My current goal is to learn how dependent typed languages are implemented and write a self-hosted dependent typed language, but I have little spare time and keep getting side-tracked.