Extending abramsky's lazy lambda calculus: (Non)-conservativity of embeddings

Manfred Schmidt-Schauß, Elena MacHkasova, David Sabel

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    5 Scopus citations

    Abstract

    Our motivation is the question whether the lazy lambda calculus, a pure lambda calculus with the leftmost outermost rewriting strategy, considered under observational semantics, or extensions thereof, are an adequate model for semantic equivalences in real-world purely functional programming languages, in particular for a pure core language of Haskell. We explore several extensions of the lazy lambda calculus: Addition of a seq-operator, addition of data constructors and case-expressions, and their combination, focusing on conservativity of these extensions. In addition to untyped calculi, we study their monomorphically and polymorphically typed versions. For most of the extensions we obtain non-conservativity which we prove by providing counterexamples. However, we prove conservativity of the extension by data constructors and case in the monomorphically typed scenario.

    Original languageEnglish (US)
    Title of host publication24th International Conference on Rewriting Techniques and Applications, RTA 2013
    EditorsFemke van Raamsdonk
    PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
    Pages239-254
    Number of pages16
    ISBN (Electronic)9783939897538
    ISBN (Print)9783939897538
    DOIs
    StatePublished - Jan 1 2013
    Event24th International Conference on Rewriting Techniques and Applications, RTA 2013 - Eindhoven, Netherlands
    Duration: Jun 24 2013Jun 26 2013

    Publication series

    NameLeibniz International Proceedings in Informatics, LIPIcs
    Volume21
    ISSN (Print)1868-8969

    Conference

    Conference24th International Conference on Rewriting Techniques and Applications, RTA 2013
    CountryNetherlands
    CityEindhoven
    Period6/24/136/26/13

    Keywords

    • Conservativity
    • Contextual semantics
    • Lazy lambda calculus

    Fingerprint Dive into the research topics of 'Extending abramsky's lazy lambda calculus: (Non)-conservativity of embeddings'. Together they form a unique fingerprint.

    Cite this