The work presented in this talk is part of a bigger project, which intends to give semantics to proof search. In this talk we present some general steps which are necessary to achieve such a semantics, and focus on one aspect, namely how to model backtracking in intuitionistic logic via continuations.

The first step consists of giving semantics to partial, possibly incompleteable proofs. We use polynomial categories for this purpose. The universal property of these categories ensures that a partial proof can be completed to a proof iff one can find a substitution consisting only of ground terms for the indeterminates in the polynomial category. The left-rules of the sequent calculus force us to consider also a Kripke-style semantics where the information contained in the Kripke-worlds is the substitution arising from modelling the implication left-rule.

In this paper we model backtracking by embedding intuitionistic logic into classical logic. Hence in a second step we extend these polynomial categories and the Kripke-semantics to the lambda-mu-nu-calculus, a term calculus for classical logic. In this semantics, a switch in the focus on the right-hand side corresponds to applying a continuation in functional languages.

When we embed LJ-proofs with backtracking into LK and translate these proofs into the semantics we have developed, we realise that backtracking in LJ-proofs gives rise to switching the right-hand side in the LK-proofs resulting from the embedding, and hence to continuations.

This is joint work with David Pym.