LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
Wednesday 22nd January 1997, 3.30pm

* NOTE NONSTANDARD TIME AND DAY *

Title: Proof Nets as Formal Feynman Diagrams

Speaker: Prakash Panangaden (McGill, Canada)

Linear logic appears to have many curious, possibly co-incidental, connections with quantum field theory. In this talk I will show how one can give an interpretation of proof nets as Feynman diagrams. More porecisely, with each proof nets is associated a formal "integral" constructed inductively from the net. Certain formal rules are introduced for computing with these integrals. We show that the process of simplification of these integrals automatically performs cut elimination. Furthermore, the exponential types are modelled as exponentials. The correspondence between nets and the formal integrals is very similar to the correspondence between Feynman diagrams and the integrals corresponding to terms in the perturbation expansion of a Quantum Field Theory. Thus our analogy is not a mere pictorial resemblence of graphical structures but actually extends to a correspondence between integrals.