Complexity of Type Inference
This paper contains the English version of my Master's thesis [6] written about 22 years ago under supervision of Jerzy Tiuryn. Its main result is the proof of PTIME- completeness of the type reconstruction problem for simply typed lambda calculus. About the time I had the English paper ready, a much simpler proof [3] by John Mitchell (later published in [4]) was announced. Therefore my thesis remained an unpublished manuscript, but has been referenced to in a number of other papers. The TEX sources went lost in the meantime, so the present paper has been re-typed from scratch, but is almost identical to the original one written many years ago.
complexity typed lambda calculus simple types typability ptime