. A new class of higher order rewriting systems, called Interaction Systems (IS's), was introduced by the author in [2]. Interaction Systems provide a nice integration of the functional paradigm with a rich class of data structures and basic control flow constructs such as conditionals and (primitive or general) recursion. In this paper, we focus on the relation between Interaction Systems and Intuitionistic Logic, via the Curry-Howard analogy. Pursuing this analogy, we define an encoding of...