The language X : circuits, computations and classical logic
Steffen van Bakel, Stéphane Lengrand, Pierre Lescanne, Fife Ky Ss, École Normale Supérieure De Lyon · 2005
Abstract. We present the syntax and reduction rules for X, an untyped language that is well suited to describe structures which we call “circuits ” and which are made of parts that are connected by wires. To demonstrate that X gives an expressive platform, we will show how, even in an untyped setting, that we can faithfully embed algebraic objects and elaborate calculi, like the naturals, the λcalculus, Bloe and Rose’s calculus of explicit substitutions λx, and Parigot’s λµ. 1