Computation with classical sequents

Abstract

$\X$ is an untyped continuation-style formal language with a typed subset that provides a Curry–Howard isomorphism for a sequent calculus for implicative classical logic. $\X$ can also be viewed as a language for describing nets by composition of basic components connected by wires. These features make ${\X}$ an expressive platform on which many different (applicative) programming paradigms can be mapped. In this paper we will present the syntax and reduction rules for $\X$ ; in order to demonstrate its expressive power, we will show how elaborate calculi can be embedded, such as the λ-calculus, Bloo and Rose's calculus of explicit substitutions λx, Parigot's λμ and Curien and Herbelin's $\lmmt$ . ${\X}$ was first presented in Lengrand (2003), where it was called the λξ-calculus. It can be seen as the pure untyped computational content of the reduction system for the implicative classical sequent calculus of Urban (2000).