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.