Proof search constitutes an interesting form of computation, for example, at the heart of logic programming languages or theorem provers. In reductive proof search (proof search based on reduction of conclusions of inference rules to their premises), proofs are naturally generalised by solutions, comprising all (possibly infinite) structures generated by locally correct, bottom-up application of inference rules.

In this seminar, we explain the basic ideas of an approach for analysing reductive proof search that builds on the Curry-Howard

correspondence between proofs and typed lambda-terms, and relies on the representation not only of individual solutions, but actually of

the entire solution space of proof search problems. Two equivalent representations are considered, one through a co-inductive lambda-calculus, and the other through a lambda-calculus with fixed points. Our case study is intuitionistic implicational logic, and a cut-free sequent calculus proof system (whose proofs are in 1-1- correspondence with simply-typed lambda-terms in eta-long beta-normal form), for which decidability results for existence and (in)finiteness of solutions are obtained.