(talk proposal for Days in Logic 2016) :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: A coinductive approach to analysis of proof search Luís Pinto, CMAT and DMA, University of Minho, Portugal :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: (abstract) Reductive proof search is proof search based on reduction of conclusions of inference rules to their premises. In this talk we explain the basic ideas of a coinductive approach to analyse reductive proof search, that builds on the Curry-Howard correspondence between proofs and typed lambda-terms, where not only the outcome of successful searches, but actually the entire search process is represented by typed lambda-terms. 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. The starting point of our approach is the observation that in reductive proof search proofs are naturally generalised by solutions, comprising all (possibly infinite) structures generated by locally correct, bottom-up application of inference rules, and such infinite structures are naturally captured by coinductive proof terms (potentially infinitely deep). Then, a coinductive lambda-calculus with formal sums (to express alternatives in the search process) is able to adequately represent the entire solution space of a sequent. The approach involves the development of an equivalent finitary repsentation of solution spaces, based on a companion finitary lambda-calculus with sums and a fixed-point operator (which compensates for the absence of coinductive proof-terms and is able to express cycles in the search process). We use these finitary representations to study solvability predicates, which ask, not only for the existence, but also for the (in)finiteness of solutions, and we obtain simple syntax directed recursive procedures to decide these predicates. This is joint work with José Espírito Santo (CMAT and DMA, University of Minho, Portugal) and Ralph Matthes (IRIT, CNRS and University of Toulouse III, France. ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::