Complexity of Type Inference

Issue title: From Mathematical Beauty to the Truth of Nature: to Jerzy Tiuryn on his 60th Birthday

Article type: Research Article

Authors: Tyszkiewicz, Jerzy

Affiliations: Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warsaw, Poland. J.Tyszkiewicz@mimuw.edu.pl

Note: [] Address for correspondence: Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warsaw, Poland

Abstract: 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.

Keywords: typed lambda calculus, simple types, typability, complexity, PTIME

DOI: 10.3233/FI-2010-329

Journal: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 289-301, 2010