Types for Proofs and Programs - Miculan, Marino; Honsell, Furio; Kanade, Takeo; Scagnetto, Ivan (Springer Berlin Heidelberg, 2008)