We present a Counting Algorithm that computes the number of λ-terms in β-normal form that have a given type τ 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 τ.