Typing and convergence in the lambda calculus LeivantDaniel 2001 Computer Science Department