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 $`l$-calculus, Bloe and Rose's calculus of explicit substitutions \Lx, and Parigot's~$`l`m$.

Appeared as;

@Inproceedings{vBLL'05,

Author = "S. van Bakel and S. Lengrand and P. Lescanne",
Title = "The language \X: circuits, computations and Classical Logic", Booktitle = "Proceedings of Ninth Italian Conference on Theoretical Computer Science (ICTCS'05), Siena, Italy",
Editor = "Mario Coppo and Elena Lodi and G. Michele Pinna",
Series = "Lecture Notes in Computer Science",
Volume = "3701",
Year = "2005",
Publisher = "Springer-Verlag",
Pages = "81-96" }