Natural deduction systems for the lambda-cube?

Hi list,

I've been working a system of natural deduction that is a sort of a
natural deduction version for the systems in the \lambda-cube, and I
just realized that probably other people could have also attempted to
do that before me, and that I should take a look at their papers...

Anyone knows of any work in that direction?

  Thanks in advance, cheers,
    Eduardo Ochs