Intuitionistic and intermediate logics in CoS

Hi,
I am currently working on formalizing intuitionistic and intermediate
logics (Dummett's LC and first-order Goedel logic) in CoS.
I have a draft paper written; if any of you happen to be working on the 
same thing, or
are interested, please let me know and I can send the paper to you.
You can find the abstract below.

Best,
-Alwen

--

A local system for intuitionistic logic

Abstract:
This paper presents systems for  first-order intuitionistic logic
and several of its extensions in which all the propositional 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 rules.
We show that the contraction rules can be restricted to the atomic ones,
provided we employ deep inference, i.e., to allow rules to apply anywhere
inside logical expressions. We further show that the use of deep 
inference allows for
modular extensions of intuitionistic logic to Dummett's intermediate 
logic LC,
Goedel logic and classical logic. We present the systems in the calculus 
of structures,
a proof theoretic formalism which supports deep-inference. Cut elimination
for these systems are proved indirectly by simulating the cut-free 
sequent systems,
or the hypersequent systems in the cases of Dummett's LC and Goedel logic,
in the cut free systems in the calculus of structures.