### SPAM Talk: Proof theory for SPAMmers

**Speaker:**
Charles Stewart,
Technische Universitaet Dresden
**When & Where:** 12:30pm, Friday, March 31, 2006, Room 200 AKW

**Abstract:**

Logic has entered the design of programming languages, besides Shannon's
venerable coding of propositional logic, mainly through two streams that
became applied in the 1970s:

- Proofs as programs (aka. Curry-Howard, or formulae-as-types)

- Proof search as computation

Both of these streams ultimately flow from the work of Gerhard Gentzen in the
1930s on the natural deduction calculus and the sequent calculus, but
despite their theoretical heritage being essentially the same, they lead to
rather dissimilar application.

I'll explore the nature of this divergence through a rapid tutorial on
structural proof theory and talk about techniques that can bridge this divide
ending with a brief survey of new developments in proof theory that I think
are worth watching.