Lightweight soundness for towers of language extensions

A. Serrano, J. Hage

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

2 Citations (Scopus)


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
Subtitle of host publicationPEPM 2017
PublisherAssociation for Computing Machinery
Number of pages12
ISBN (Print)9781450347211
Publication statusPublished - 2 Jan 2017


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

Cite this