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:
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.