Traditionally, logics are formulated as systems of deductive inference in which proofs are constructions which derive conclusions from given assumptions. However, in computing, many problems are naturally formulated as questions of reductive inference in which the correctness of a given putative conclusion must be shown by reduction, commonly formulated as proof-search in a given formal system, to established acceptable assumptions. Examples of this phenomenon include type-inference, parsing, program correctness and internet information retrieval. Typically, such examples are described as long and complex formal texts. Consequently, algorithmic proof-search is a fundamental enabling technology throughout the computing sciences. Moreover, the reductive view of inference represents an alternative view of logic, just as fundamental as the deductive one, which is largely undeveloped.

So far, the theory of proof-search has developed mostly along proof-theoretic lines but using many type-theoretic techniques. The utility of type-theoretic methods suggests that semantic methods of the kind found to be valuable in the semantics of programming languages should be useful in tackling the main outstanding difficulty in the theory of proof-search, i.e., the representation of intermediate stages in the search for a proof. The space of searches is much larger than the space of proofs: An adequate semantics would represent both the space of searches and the space of proofs and give an account of the recovery of proofs (which are extensional objects) from searches (which are more intensional objects). It would distinguish between different proof-search strategies and permit analyses of their relative merits.

This seminar helps to establish a program to build such a semantics. To this end, we propose the following foci for the seminar:

• Reductive vs. deductive logic: their logical, mathematical and computational properties;
• Proof-search in type-theoretic languages: the role of typing constraints during proof-search;
• Proof- and model-theoretic analyses of search spaces: the search-oriented counterparts to traditional proof theory and model theory;
• Intensional semantics for proof-search: specific intensional and computational models based on structures such as games, continuations and realizability;
• Applications of proof-theoretic and semantic techniques to the design and implementation of theorem provers.