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