Thumbnail
Access Restriction
Open

Author Barthe, Gilles ♦ Kamareddine, Fairouz ♦ Ríos, Alejandro
Source CiteSeerX
Content type Text
File Format PDF
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Explicit Substitution ♦ Explicit Substitution Calculus ♦ Control-like Operator ♦ Reduction Rule ♦ Classical Logic ♦ First Study ♦ Introduction Explicit Substitution ♦ Call-by-name Continuation-passing Style Translation ♦ Strong Normalisation ♦ Extended Translation Preserve ♦ First Example ♦ Normalisation Procedure ♦ Strong Normalisation Property ♦ Cps Translation ♦ Particular Application ♦ Typed Version
Abstract . The \Delta-calculus is a -calculus with a control-like operator whose reduction rules are closely related to normalisation procedures in classical logic. We introduce \Deltaexp, an explicit substitution calculus for \Delta, and study its properties. In particular, we show that \Deltaexp preserves strong normalisation, which provides us with the first example --moreover a very natural one indeed-- of explicit substitution calculus which is not structure-preserving and has the preservation of strong normalisation property. One particular application of this result is to prove that the simply typed version of \Deltaexp is strongly normalising. In addition, we show that Plotkin's call-by-name continuation-passing style translation may be extended to \Deltaexp and that the extended translation preserves typing. This seems to be the first study of CPS translations for calculi of explicit substitutions. 1 Introduction Explicit substitutions were introduced by Abadi, Cardelli, Curien and L...
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study