(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.Robert Recorde Room

Department of Computer Science