Computational soundness of a call by name calculus of recursively-scoped records

Elena Machkasova

    Research output: Contribution to journalConference articlepeer-review

    1 Scopus citations

    Abstract

    The paper presents a calculus of recursively-scoped records: a two-level calculus with a traditional call-byname λ-calculus at a lower level and unordered collections of labeled λ-calculus terms at a higher level. Terms in records may reference each other, possibly in a mutually recursive manner, by means of labels. We define two relations: a rewriting relation that models program transformations and an evaluation relation that defines a small-step operational semantics of records. Both relations follow a call-by-name strategy. We use a special symbol called a black hole to model cyclic dependencies that lead to infinite substitution. Computational soundness is a property of a calculus that connects the rewriting relation and the evaluation relation: it states that any sequence of rewriting steps (in either direction) preserves the meaning of a record as defined by the evaluation relation. The computational soundness property implies that any program transformation that can be represented as a sequence of forward and backward rewriting steps preserves the meaning of a record as defined by the small step operational semantics. In this paper we describe the computational soundness framework and prove computational soundness of the calculus. The proof is based on a novel inductive context-based argument for meaning preservation of substituting one component into another.

    Original languageEnglish (US)
    Pages (from-to)150-164
    Number of pages15
    JournalElectronic Notes in Theoretical Computer Science
    StatePublished - Dec 1 2007
    Event7th International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2007, as part of the 4th Federated Conference on Rewriting, Deduction, and Programming, RDP 2007 - Paris, France
    Duration: Jun 25 2007Jun 25 2007

    Keywords

    • Calculus
    • Call-by-name
    • Computational soundness
    • Recursively-scoped records

    Fingerprint Dive into the research topics of 'Computational soundness of a call by name calculus of recursively-scoped records'. Together they form a unique fingerprint.

    Cite this