There isn't a single book that covers all of it... Bend's theory touches various domains (dependent types, substructural types, termination). And then there's t

There isn't a single book that covers all of it... Bend's theory touches various domains (dependent types, substructural types, termination). And then there's the runtime, compiler, GPU kernels... If you mean about the type theory specifically, "Type Theory and Formal Proof by Nederpelt and Geuvers" is a good introduction. Not sure what I'd recommend on linear types, no book I know of is very introductory? Perhaps "Idris 2: Quantitative Type Theory in Practice", which is a language with similar foundations to Bend, and the author wrote a book on it (and inspired myself!)