@yoriyuki Not a textbook, but CMU has a higher-order typed compilation (HOT comp) course:
- Karl Crary iteration: https://www.cs.cmu.edu/~crary/hotc/ talks about how to compile an ML language down to C. There’s no lecture notes but project code are available.
- Frank Pfenning iteration: https://www.cs.cmu.edu/~fp/courses/15417-s25/ talks about compiling substructural functional languages. Frank write very good lecture notes!