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.