I really recommend [56] M. H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard isomorphism. Elsevier, 2006 on this topic. I found it online. It is very s

I really recommend [56] M. H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard isomorphism. Elsevier, 2006 on this topic. I found it online. It is very self-contained and explains some interesting topics such as relation of intuitionist and classical logic.