We will present the language X that describes circuits by composition of basic components, and has been designed to give a Curry-Howard-de Bruijn correspondence to the sequent calculus for classical logic. In this talk, we present its syntax and its reduction rules. The symmetry of the cut-elimination procedure is reflected by a symmetry in the reduction relation. To demonstrate the expressive power of X, we will show how, even in an untyped setting, more and more elaborate calculi can be embedded into X. We describe how the symmetrical reductions of X account for the call-by-name and call-by-value evaluations.
We will discuss implementation issues, using a term graph rewriting technique, and present a non-standard notion of decidable type assignment both on terms and graphs.