title ``Equivalence of Logics: the categorical proof theory perspective''

Valeria de Paiva
PARC, USA


The categorical proof theory approach to logic has been around since at least 
the early sixties (cf. the pioneering work of Lambek and Lawvere) and it has
 been very sucessful. As evidence, consider the number of practioners, the 
quality  of international research projects (e.g. 
CLiCS I and II, Types, APPSEM I and II) and the sheer
amount of research, papers, theses, monographs, software, etc generated. 
The picture is less rosy, however, if you consider the impact it has had on 
logic itself.

In this ``propaganda''  talk I will describe the basic ideas of  categorical 
proof thery, some of its successes and some of its possibilities as far as 
applications back in logic are concerned. Thus I hope to explain the identity
 criteria that we arrive at, when confronted with the problem of deciding when
 two logical systems should be taken as ``the same'', using the perspective of
categorical proof theory. As a paradigmatic example I will be discussing
(mostly Intutitionistic)  Linear Logic, the main source  of my intuitions.