Type Theory and Formal Proof: An Introduction

[QuangTung97]

I think this book is very good for learning Type Theory, includes Untyped Lambda Calculus, many systems of the Lambda Cube and extended with Definitions.

[Sebastien-sys]

This book is not very good, it"s excellent , especially for those who who to discover lambda calculus. There is solutions to selected exercices here : https://wsinrpn.win.tue.nl/CUP-C-Selected-exercises.pdf