Types for Proofs and Programs - Berardi, Stefano; Damiani, Ferruccio; Kanade, Takeo; de Liguoro, Ugo (Springer Berlin Heidelberg, 2009)