The language X: circuits, computations and Classical Logic
Résumé
X is an untyped language for describing circuits by composition of basic components. This language is well suited to describe structures which we call "circuits" and which are made of parts that are connected by wires. Moreover X gives an expressive platform on which algebraic objects and many different (applicative) programming paradigms can be mapped. In this paper we will present the syntax and reduction rules for X and some its potential uses. To demonstrate the expressive power of X, we will show how, even in an untyped setting, elaborate calculi can be embedded, like the naturals, the $`l$-calculus, Bloe and Rose's calculus of explicit substitutions lambda-x, Parigot's lambda-mu and Curien and Herbelin's lambda-mu-mu~.
X est un langage non typé conçu pour d écrire les circuits par composition de "briques" de base.Ce langage s’adapte parfaitement à la description des structures que nous appelons "circuit" et qui sont faites de composants connectés par des fils. De plus, X fournit une plateforme expressive sur laquelle des objets algébriques et de nombreux paradigmes de programmation (applicative) de toute sortes peuvent être appliqués. Dans ce rapport, nous présenterons la syntaxe de X, ses règles de réduction et certaines de ses utilisations potentielles. Pour mettre en lumière le pouvoir expressif de X, nous montrerons comment, même dans un cadre non typé,on peut y plonger des calculs relativement sophistiqués,comme les entiers naturels,le -calcul,le lambda-calcul de substitutions explicites lambda de Bloe et Rose, le calcul lambda-mu de Parigot et le calcul lambda-mu-mu~de Curien et Herbelin
Origine : Fichiers produits par l'(les) auteur(s)
Loading...