A local system for intuitionistic logic

Dear members of Frogs list,
I recently have some preliminary results on formalizing
a local system for intuitionistic logic in the calculus of structures.
I have a paper ready, and I'll be glad if you can have a look
and let me know of your comments or suggestions.
Abstract and the links to the paper are given below.

Best,
-Alwen

Title: A Local System for Intuitionistic Logic: Preliminary Results
Links:
 http://www.loria.fr/~tiu/localint.ps  (postscript file)
 http://www.loria.fr/~tiu/localint.pdf (pdf)

Abstract
--
This paper presents a system for  intuitionistic logic in which all the 
rules are
local, in the sense that, in applying the rules  of the system, one 
needs only a fixed
amount of information about the logical expressions involved.
The main source of non-locality is the contraction rule.
We show that the contraction rule can be restricted to the atomic one,
provided we employ {\em deep-inference}, i.e., to allow rules
to apply anywhere inside logical expressions.
However, the use of deep-inference and the asymmetry of the logic
give rise to the context-dependency of the rules. We further show 
that this context dependency can be removed by introducing polarities into
logical expressions. We present the system in the calculus of structures,
a proof theoretic formalism which supports deep-inference. This system
is shown to be sound and complete  with respect to Gentzen's LJ
and an equivalent notion of cut-elimination is proved.