On the expressive power of schemes

We present a calculus, called the scheme-calculus, that permits to express natural deduction proofs in various theories. Unlike λ-calculus, the syntax of this calculus sticks closely to the syntax of proofs, in particular, no names are introduced for the hypotheses. We show that despite its non-determinism, some typed scheme-calculi have the same expressivity as the corresponding typed λ-calculi.