# Proof Nets as Formal Feynman Diagrams

Prakash Panangaden (McGill, Canada) LFCS Theory Seminar Room 2511, JCMB, King's Buildings Wednesday 22nd January 1997, 3.30pm

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 precisely, 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 resemblance of graphical structures but actually extends to a correspondence between integrals.