Re: Calculus of structures and sequent calculus

> The case with duplication of unbounded-size derivations might be handled
> with some kind of ressource-management explicit calculus, so it is not
> really an obstruction.

I have the impression that, as soon as you enrich enough the objects
you're working on, say with pointers, then everything can be done
locally. So "local" becomes a meaningless notion.

 
> Is that kind of process has any chance to exist in CoS? Maybe it is not
> with cut but with another class of rules?

Oh, definitely. These processes are all over the place. See the proofs
of the "decomposition" theorems in Lutz' and my thesis. The
transformation you give also occurs all over the place, e.g. p.70 in
my thesis.

 
> I hope I have time to explain all this next week!

Looking forward to it!

-Kai