In short, we will look at the Curry-Howard Correspondence in different scenarios while, especially, focusing on computational consequences of the proof theoretical choices that need to be made. That is, we will presentan overview of several different styles of presenting symbolic logics, point out their differences and similarities, and look at the resulting computational meanings which are not all as would be expected.
In the end this will allow us to present a calculus of cut elimination which bears striking resemblance to know lambda calculi with explicit substitutions.
The talk will be largely self contained although familarity with the lambda calculus and its different typing styles will be a plus.