I enjoyed Benjamin Pierce's book Types and Programming Languages: https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/ He provi

I enjoyed Benjamin Pierce's book Types and Programming Languages: https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/ He provides theory and code that starts from untyped lambda calculus and progresses to typed lambda calculus, system F, and higher-order system. Note, the article above was written by Barendregt who summarized high-order systems in terms of the "lambda cube". The Pierce book provides enough theory and context to understand why that's important by the time he gets to it in chapter 30.