Logical foundations of functional programming - Huet, Gérard (The UT Year of Programming Series, 1990)