An extension of the proof/program correspondence is given
in the ambient logic of classical second order propositional
calculus. Using a notion of realizability in a concurrent extension of
lambda-c-calculus, it is shown that a certain class of purely
disjunctive closed formulas are specifying synchronisation protocols.
