Proof theory is interested mainly in the questions "What is a proof?" and
"When are two proofs equal?". Girard answered these questions in 1986 for
linear logic by developing proof nets. Proof nets constitute a proof system
that abstracts away syntactic bureaucracy (e.g. the order in which subgoals
are proved) and thus gets close to the real essence of proofs.
In this talk, I will turn the focus towards intuitionistic logic, a
fragment of classical logic in which all proofs must be constructive. This
logic is important for example as the theoretical foundation of functional
programming.
I will present a translation of the simply typed lambda-calculus, a
well-examined proof system for intuitionistic logic, into a new kind of
proof nets that are especially suited for intuitionistic logic. I will
analyze the meaning and shape of these nets. Moreover, I will introduce a
strongly normalizing and confluent reduction procedure for the new proof
nets. The result of these explorations is a new notion of the equivalence of
intuitionistic proofs.