Lightweight soundness for towers of language extensions
Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and …, 2017•dl.acm.org
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 …
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 …
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.
ACM Digital LibraryShowing the best result for this search. See all results