by R.A.G. Seely
ABSTRACT:
We give a definition of a ``linear fibration'', which is a hyperdoctrine model of polymorphic linear logic, and show how to internalise the fibration, generating topos models. This gives a constructive set theoretical context for the logic of Petri nets, as recently developed by N. Marti-Oliet and J. Meseguer. Also, we sketch how this can be further extended to include the exponential operator ! . In this context, the topos model we construct can be embedded in the model constructed by A.M. Pitts.
This appeared in
C.R. Math. Rep. Acad. Sci. Canada - Vol. XII, No. 1, February 1990