Journal of Logic and Computation Advance Access originally published online on February 16, 2007
Journal of Logic and Computation 2008 18(2):229-238; doi:10.1093/logcom/exm001
| ||||||||||||||||||||||||||||||||||||||||||||||||
Original Articles |
M. H. Newman's Typability Algorithm for Lambda-calculus
Mathematics Department, Swansea University, Swansea SA2 8PP, UK.
E-mail: j.r.hindley{at}swan.ac.uk
Received 30 January 2006.
| Abstract |
|---|
This article is essentially an extended review with historical comments. It looks at an algorithm published in 1943 by M. H. A. Newman, which decides whether a lambda-calculus term is typable without actually computing its principal type. Newman's algorithm seems to have been completely neglected by the type-theorists who invented their own rather different typability algorithms over 15 years later.
Keywords: Newman; typable; stratified; lambda-calculus; typability algorithm