Correct and Abstract Semantics Lifting for Domain-Specific Language Implementation

Implementing domain-specific languages (DSLs) through higher-order functions and macros often leads to abstraction leakage, diminishing their user-friendliness. This paper introduces a semantics-lifting framework to address this challenge. The proposed framework offers a general algorithm to derive DSL semantics independent of the host language based on host semantics and translation rules. It formulates cor- directness and abstraction properties, ensuring the semantics lifting process maintains these properties. Additionally, the paper explores the necessary assumptions for achieving correct and abstract lifted semantics, demonstrated through the implemented system Osazone. Case studies across various host languages, including functional and imperative types, confirm the flexibility and reliability of the framework, ensuring the lifted DSL semantics preserve correctness and abstraction integrity throughout.