Type Inference Algorithm for Pure Type Systems

摘要

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