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.