A Type Inference Algorithm for Pure Type Systems

A large class of typed lambda calculi can be described. in a uniform way as Pure Type Systems(PTS's). This includes for instance ~he second-order lambda calculus and the Cal-culus of Constructions. There are several implementations of PTS's such as COQ, LEGO or CONSTRUCTOR. It is important to know that these implementantions are actually correct. In this paper we present an efficient algorithm for infering types for singly sorted Pure Type Systems and prove its correctness.