The Little Typer by Daniel P. Friedman and David Thrane Christianse. It's basically one long book of examples building on each other to show the semantics of a

The Little Typer by Daniel P. Friedman and David Thrane Christianse. It's basically one long book of examples building on each other to show the semantics of a dependently typed programming language. It inspired me to learn some type theory and made me interested in mathematical logic more generally.