Explicit Substitutions for the Lambda-Mu-Calculus.

Abstract

(eng) 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.