A Coinductive Approach to Proof Search Through Typed Lambda-Calculi