Department of Mathematics and Statistics
University of Ottawa
(visiting the Computing
Lab, Oxford)
2pm Friday 17th December 2004
Room 2511, JCMB, King's Buildings
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 & Arbib.