  We introduce a Curry-Howard correspondence for a large class of intermediate
logics characterized by intuitionistic proofs with non-nested applications of
rules for classical disjunctive tautologies (1-depth intermediate proofs). The
resulting calculus, we call it $\lambda_{\parallel}$, is a strongly normalizing
parallel extension of the simply typed $\lambda$-calculus. Although simple, the
$\lambda_{\parallel}$ reduction rules can model arbitrary process network
topologies, and encode interesting parallel programs ranging from numeric
computation to algorithms on graphs.
