# Geometry of Interaction and the Dynamics of Proofs

Philip Scott 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.