Types for Proofs and Programs - Filliâtre, Jean-Christophe; Kanade, Takeo; Paulin-Mohring, Christine; Werner, Benjamin (Springer Berlin / Heidelberg, 2006)