Semantics and logics of computation - Pitts, A. M. (Andrew M.); Dybjer, Peter (Cambridge University Press, 1997)