Geometry of Interaction and the Dynamics of Proofs

Photograph of Philip Scott

Philip Scott

(Ottawa)

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 a profound series of papers starting in 1988. Using techniques from functional analysis and operator algebras, Girard's work (and following work by Danos, Regnier, et al) offers novel insights into the operational and denotational semantics of proofs. More recently, work by Hyland, Abramsky, and others has led to new insights into GoI. We shall survey some of the basic features of GoI, and give an introduction to some of my recent results with Esfan Haghverdi analyzing and axiomatizing the foundations of GoI.
Tuesday 2nd November 2004, 14:00
Robert Recorde Room
Department of Computer Science