## SSS Abstracts |

In partial fulfillment of the speaking requirement.

Backward proof search, however, is not always the best proof search strategy. Linear logic, a logic for reasoning about state, is one example where backward search contains undesirable non-deterministic choices that entirely disappear when reasoning forwards-- starting from known facts and inferring new facts using the logical rules until the goal proposition is inferred. Because focusing is so beneficial in the backward direction, the obvious question to ask is whether the insights of focusing can also be applied to forward search.

In this talk I will sketch the forward search strategy for a fragment of linear logic and answer precisely this question. No familiarity with linear logic is assumed.

Based on joint work with Frank Pfenning.

In partial fulfilment of the speaking requirement.

In partial fulfillment of the speaking requirement

Joint work with Carlos Guestrin, Anupam Gupta, Jon Kleinberg and Ajit Singh. In partial fulfillment of the CSD speaking requirement.

This talk is in partial fulfilment of the speaking requirement.

Joint work with Andrew Moore and Ting Liu. In partial fulfillment of the CSD speaking requirement.

Joint work with Doug L. James

In Partial Fulfillment of the Speaking Requirement

with: Frank Pfenning

in partial fulfillment of the Speaking Requirement

In this talk, I will start with reviewing, for a general computer science audience, of prior work in type theory. I will motivate our work as a natural evolution of these ideas.

This is joint work with Karl Crary. The talk is in partial fulfilment of the CSD speaking requirement.

In Partial Fulfillment of the Speaking Requirement

However, these formal proofs typically blow up in size compared to "paper" proofs, because every last formal detail of the proof must (in principle) be included. This talk describes an attempt to address this problem: it turns out that a more compact representation of proofs comes naturally out of thinking about what it means for a formal system to be an adequate representation of the informal mathematics it’s meant to encode.

(In Partial Fulfillment of the Speaking Requirement)