Type-Checking Systems with Particular Applications to Functional Languages. - H. K. F. Yeung (1976)