Types for Proofs and Programs - Altenkirch, Thorsten; Kanade, Takeo; McBride, Conor; Kittler, Josef; McBride, Connor (Springer Berlin Heidelberg, 2007)