  A new, comprehensive approach to inhabitation problems in simply-typed
lambda-calculus is shown, dealing with both decision and counting problems.
This approach works by exploiting a representation of the search space
generated by a given inhabitation problem, which is in terms of a
lambda-calculus for proof search that the authors developed recently. The
representation may be seen as extending the Curry-Howard representation of
proofs by lambda-terms, staying within the methods of lambda-calculus and type
systems. Our methodology reveals inductive descriptions of the decision
problems, driven by the syntax of the proof-search expressions, and the end
products are simple, recursive decision procedures and counting functions.
