Francois Lamarche says:
I still think that if I started working again in this field, the problem I would zero in would be to get rid of the permutation groups,
This would be a great pity. Girard's coherence spaces (see "Proofs and Types"), ordinary relational algebra (in which Shroeder identified the par, writing +, for it, I think, in 1895) and my model with groupoids all illustrate a common theme in the workings of models of linear logic. In all of these structures, there are extremely natural ways of defining the structure on disjoint unions and cartesian products, and of turning the structure inside out or upside down. These turn out to be the additive, multiplicative and negative connectives in linear logic. There are less natural ways of defining the structure on powersets, finite powersets and other variations on this theme. These are the exponentials. It is important to note that there are several different exponential operations available to interpret ! and ? . Girard got function spaces out of such constructions (as did Francois, myself and numerous other people). What I hope to show soon is how to get higher order logic too. Paul