Back to computability logic

Hello everyone. About a year ago we have collectively attempted but
failed to axiomatize various fragments of computability logic. Finding 
good deductive systems for computability logic has been on the problems 
list of the main CoS webpage since then. I see a light at the end of
the tunnel in the paper advertised below.  Its last paragraph kinda 
contains a marriage proposal to CoS, so I'd be curious to know how the
other party feels before going any farther.

The preprint is available at http://arxiv.org/abs/math.LO/0506553  
Here is the abstract:

 
                          Giorgi Japaridze

   Introduction to Cirquent Calculus and Abstract Resource Semantics 


This paper introduces a refinement of the sequent calculus approach 
called *cirquent calculus*. Roughly speaking, the difference between
the two is that, while in Gentzen-style proof trees sibling (or cousin,
etc.) sequents are disjoint and independent sequences of formulas, in
cirquent calculus they are permitted to share elements. Explicitly
allowing or disallowing shared resources and thus taking to a more
subtle level the resource-awareness intuitions underlying substructural
logics, cirquent calculus offers much greater flexibility and power
than sequent calculus does. A need in substantially new deductive tools
came with the advent of computability logic --- the semantically 
constructed formal theory of computational resources, which has
stubbornly resisted any axiomatization attempts within the framework 
of traditional syntactic approaches. Cirquent calculus breaks the ice. 
Removing contraction from the full ("classical") collection of its 
rules yields a sound and complete system for the basic fragment CL5 of
computability logic, previously thought to be "most unaxiomatizable".
Deleting the offending rule of contraction in ordinary sequent 
calculus, on the other hand, throws out the baby with the bath water,
resulting in affine logic that is strictly weaker than CL5. An implied 
claim of computability logic is that it is CL5 rather than affine logic
that adequately materializes the resource philosophy traditionally
associated with the latter. To strengthen this claim, the paper further 
introduces an abstract resource semantics and shows the soundness and 
completeness of CL5 with respect to it. Unlike the semantics of
computability logic that understands resources in a special ---
computational --- sense, abstract resource semantics can be seen as a 
direct formalization of the more general yet naive intuitions in
the "can you get both a candy and an apple for one dollar?" style. The
inherent incompleteness of affine or linear logics, resulting from the
fundamental limitations of the underlying sequent-calculus approach, is 
apparently the reason why such intuitions and examples, while so 
heavily relied on in the popular linear-logic literature, have never
really found a good explication in the form of a mathematically strict
and intuitively convincing semantics. The paper is written in a style
accessible to a wide range of readers. Some basic familiarity with
computability logic, sequent calculus or linear logic is desirable only 
as much as to be able to duly appreciate the import of the present
contribution.