  In reductive proof search, proofs are naturally generalized by solutions,
comprising all possibly infinite structures generated by locally correct,
bottom-up application of inference rules. We propose an extension of the
Curry-Howard paradigm of representation, from proofs to solutions: to represent
solutions by possibly infinite terms of a dedicated lambda-calculus. This new,
comprehensive approach to proof search is exemplified with the sequent calculus
LJT for intuitionistic implication logic. A finitary representation is
proposed, comprising lambda-terms extended with a formal greatest fixed point,
and a type system that can be seen as a logic of coinductive proofs. In the
finitary system, fixed-point variables enjoy a relaxed form of binding that
allows the detection of cycles through the type system. Formal sums are used to
express alternatives in the search process. Moreover, formal sums are used in
the coinductive syntax to define "decontraction" (contraction bottom-up) - an
operation whose theory we initiate in this paper. As a semantics, we assign a
coinductive lambda-term to each finitary term. The main result is the existence
of an equivalent finitary representation for any full solution space expressed
coinductively. This result is the main ingredient in the proof that our logic
of coinductive proofs is sound and complete with respect to the coinductive
semantics. These results are the foundation for an original approach to proof
search, where the search builds the finitary representation of the full
solution space, and the a posteriori analysis typically consisting in applying
a syntax-directed procedure or function. The paper illustrates this for proof
search and inhabitation problems in the simply-typed lambda-calculus, reviewing
results detailed elsewhere, and including new results that obtain extensive
generalizations of the so-called monatomic theorem.
