We will present the language X that describes a calculus of connections that has been designed to give a Curry-Howard correspondence to Gentzen's sequent calculus for implicative classical logic.
The symmetry of the cut-elimination procedure for proofs is reflected by a symmetry in the reduction relation on X. 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 show how 'normal' calculi like the lambda calculus, lambda-mu and Curien-Herbelin's calculus can be safely embedded in X.
We will finish by defining what should be the natural intersection-union type system for X, but argue that it (surprisingly) does not generate filter semantics.
The talk is a summary of work performed over the last nine years, in part in collaboration with Stephane Lengrand and Pierre Lescanne.