The correctness of Newman’s typability algorithm and some of its extensions

We study Newman’s typability algorithm (Newman, 1943) [14], for simple type theory. The algorithm originates from 1943, but was left unnoticed until (Newman, 1943) [14], was recently rediscovered by Hindley (2008) [10]. The remarkable thing is that it decides typability without computing a type. We give a modern presentation of the algorithm (also a graphical one), prove its correctness and show that it implicitly does compute the principal type. We also show how the typing algorithm can be extended to other type constructors. Finally we show that Newman’s algorithm actually includes a unification algorithm.