Explicit Substitutions for the Lambda-Mu-Calculus.

Philippe Audebaud (1)

1 LIP - Laboratoire de l'Informatique du Parallélisme

We present a confluent rewriting system wich extends a previous calculus for the Lambda-Calculus (Levy, Hardin) to Parigot's untyped Lambda-Mu-Calculus. This extension embeds the Lambda- Mu-Calculus as a sub-theory, and provides the basis for a theoretical framework to study the abstract properties of implementations of functional programming languages enriched with control structures. This study gives also some interesting feedback on Lambda-Mu-Calculus on both the syntactical and semantics levels.

Nous proposons un système de réécriture confluent qui étend un précédent système avec substitutions explicites pour le lambda-calcul [Hae89] au lambda-mu-calcul non typé de Parigot Par Cette extension contient le lambda-mu-calcul comme sous-théorie, et fournit une cadre théorique de base pour l'étude des propriétés abstraites des implantations des langages fonctionnels étendus avec des structures de contrôle. Cette étude fournit également un éclairage nouveau sur le lambda-mu-calcul à la fois au plan syntaxique et sémantique

Mots clés: Lambda-Mu Calculus; Rewriting Systems

Mots clés: Systèmes de Réecriture; Lambda-Mu-Calcul

Domaines: Informatique [cs]

Philippe Audebaud. Explicit Substitutions for the Lambda-Mu-Calculus.. [Research Report] LIp RR-1994-26, Laboratoire de l'informatique du parallélisme. 1994, 2+14p. ⟨hal-02102044⟩