Proofnets and Paths in Constructive Classical Logic: Too Old, Too New
Harry Mairson
I am going to talk about two ideas: one rather old, but not well
known, the other very recent but not yet worked out in detail.
First, I will discuss a transformation on proofnets which code the
MELL equivalent of continuation-passing style lambda terms. The
result of this "direct style transformation" gives a mechanical way
of generating proofnets for classical logic from the
continuation-passing style versions of lambda calculus with call/cc,
lambda-mu calculus, Filinski and other dual calculi, etc., where the
connection to polarized linear logic is pretty clear. In the second
part of the talk, I will describe how call-by-value and call-by-name
results can be extracted from such proofnets using paths and geometry
of interaction. The paths are multiple (as there are multiple
continuations), concurrent, and synchronized in their traversal of
boxes.