Lambda Calculus with Types

This handbook with exercises reveals the mathematical beauty of formalisms hitherto mostly used for software and hardware design and verification.