Lightweight soundness for towers of language extensions

A. Serrano Mena, J. Hage

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review


    It is quite natural to define a software language as an extension of a base language. A compiler builder usually prefers to work on a representation in the base language, while programmers prefer to program in the extended language. As we define a language extension, we want to ensure that desugaring it into the base language is provably sound.
    We present a lightweight approach to verifying soundness by embedding the base language and its extensions in Haskell. The embedding uses the final tagless style, encoding each language as a type class. As a result, combination and enhancement of language extensions are expressed in a natural way. Soundness of the language extension corresponds to well-typedness of the Haskell terms, so no extra tool but the compiler is needed.
    Original languageEnglish
    Title of host publicationProceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2017
    ISBN (Print)978-1-4503-4721-1
    Publication statusPublished - 2017


    Dive into the research topics of 'Lightweight soundness for towers of language extensions'. Together they form a unique fingerprint.

    Cite this