Allen Liao

Read the first half (up to encoding logical notions in λC). The first three chapters are pretty clear and easy to understand, but once it gets to type dependent on types and terms, they stopped giving syntax rules and things becomes more sloppy, requiring more work from the reader to understand the full implication of the typing system.
Would recommend this to all readers who know a bit of logic, but make sure to at least skim through the exercises and proofs portion of the text, as they become increasingly important.