They often come in pairs

[Francois Lamarche <Francois.Lamarche@loria.fr>]

Perhaps some precisions should be added to Paul's msg.

> Another model, whose types are named by countable groupoids (or by the
> corresponding presheaf toposes of G-sets) is to be found in my paper
> "Quantitative Domains, Groupoids and Linear Logic" in the proceedings
> of the 1989 Manchester CTCS.  When I was writing this paper I tried to
> get Francois Lamarche to read it, but he said he didn't know anything
> about / hated permutation representations.  Nobody else, so far as I can
> gather, has ever read it, and now I can no longer follow the most
> difficult calculations.  However, it is a very pretty model nevertheless.

Because of my thesis' work (on not-unrelated subjects to those mentioned
by Paul) I had already dealt with permutations in power types when Paul
started pushing his groupoid models. They indeed give rise to "the most
horrendous mess". This was a long time ago, my memory is vague, but I
probably told him, or hinted, that in my opinion they were most likely a
blind alley. 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, by "unraveling" them by the means of actions (the
groupoid associated with the action of a group on a set can be made much
simpler than the group itself). The point of semantics is to give you
insights about the logic, so simplicity is... a big plus.

And since I refereed his CTCS paper, I *did* read it.

Francois