In a proof system based on the deep inference methodology (as implemented in the calculus of structures), new decompositions of inference steps appear and enrich the possible shapes of proofs. In particular, the lazy context splitting embodied in the "switch" rule is a distinctive feature of this methodology, which is related in an essential way to the order of inference steps used in a proof (which can often be seen as equivalent to a sequent proof, with a particular interleaving chosen for branches).

From a Curry-Howard perspective, we are interested in the computational meaning of such a decomposition. In this talk, I will present a system for intuitionistic logic in the calculus of structures, and show how to use it as a type system for a lambda-calculus with explicit substitutions. The switch rule, seen as a typing rule, introduces a new operator performing a synchronisation (that is, a form of communication) between different parts of a term. This yields interesting observations and questions, concerning communication between "subprocesses" of a term, evaluation strategies, the implementation of functional languages and the treatment of contexts.