Counting a type's pringipal inhabitants

Sabine Broda and Luís Damas



We present a Counting Algorithm that computes the number of lambda terms in beta normal form that have a given type tau as a principal type and produces a list of these terms. The design of the algorithm follows the lines of Ben-Yelles'algorithm for counting normal (not necessarily principal) inhabitants of a type tau.