一句话：提出语义提升框架，可从宿主语言语义与脱糖规则静态派生语法糖的自包含求值规则，并保证正确性与抽象性。
语法糖在通用语言和领域特定语言中广泛使用，能提供便捷语法和更高层抽象。但传统做法把含语法糖的程序翻译回宿主语言，会造成抽象泄漏，破坏便利性并影响程序理解。本文提出语义提升（semantics lifting），旨在为语法糖静态推导自包含的求值规则。其框架包含：从宿主语言语义与脱糖规则推导宿主无关语义的通用算法；提升语义的正确性与抽象性形式化定义；保证提升语义可证明正确且抽象的充分条件。作者实现 Osazone 并开展多个案例研究，表明该方法灵活、有效，适合实现领域特定语言。
Syntactic sugar plays a crucial role in engineering programming languages. It offers convenient syntax and higher-level of abstractions, as witnessed by its pervasive use in both general-purpose and domain-specific contexts. Unfortunately, the traditional approach of translating programs containing syntactic sugars into the host language can lead to abstraction leakage, breaking the promise of convenience and hindering program comprehension. To address this challenge, we introduce the idea of semantics lifting that aims to statically derive self-contained evaluation rules for syntactic sugars. More specifically, we propose a semantics-lifting framework that consists of (i) a general algorithm for deriving host-independent semantics of syntactic sugars from the semantics of the host language and the desugaring rules, (ii) a formulation of the correctness and abstraction properties for a lifted semantics, and (iii) a systematic investigation of sufficient conditions that ensure a lifted semantics is provably correct and abstract. To evaluate our semantics-lifting framework, we have implemented a system named Osazone and conducted several case studies, demonstrating that our approach is flexible, effective, and practical for implementing domain-specific languages.
@article{GuanCYW0H24,
title = {Semantics Lifting for Syntactic Sugar},
author = {Zhichao Guan and Yiyuan Cao and Tailai Yu and Ziheng Wang and Di Wang and Zhenjiang Hu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689758}
}