I read many sections of a few volumes when trying to pick a textbook to teach a seminar in Oxford. They are really nice, which is not surprising as they have e.g. Jeremy Avigad in the editorial board. Furthermore, they are beautifully typeset. I required a more computational approach, so my favorite texts remain:
The last one is freely available, but also quite advanced as it develops all theory from the Curry-Howard isomorphism angle. I think it is ideal for advanced CS students though, and an amazing textbook due to the breadth of material it manages to cover.
* https://link.springer.com/book/10.1007/978-0-8176-4763-6
* https://www.cs.bham.ac.uk/research/projects/lics/
* https://link.springer.com/book/10.1007/978-1-4471-4129-7
* https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...
The last one is freely available, but also quite advanced as it develops all theory from the Curry-Howard isomorphism angle. I think it is ideal for advanced CS students though, and an amazing textbook due to the breadth of material it manages to cover.