Abstract: |
How do we mathematically model the dynamics of Gentzen's
cut-elimination (normalization) in proof theory? To answer this
question, J-Y Girard introduced his Geometry of Interaction (GoI)
program in an important series of papers starting in 1988. Using
techniques from functional analysis and operator algebras, Girard's
work (and later work by Danos, Regnier, et al) offers novel insights
into the operational and denotational semantics of proofs.
In recent works with Esfan Haghverdi (Indiana) we have begun a
categorical analysis and axiomatization of Girard's original approach
to GoI. We shall discuss some of this work and recent advances in
GoI, based in part on returning to early work on axiomatic infinite
sums by Higgs, and by Manes and Arbib.
|