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.
Wed 23 OctDisplayed time zone: Pacific Time (US & Canada) change
10:40 - 12:20 | |||
10:40 20mTalk | A Pure Demand Operational Semantics with Applications to Program Analysis OOPSLA 2024 Scott F. Smith The Johns Hopkins University, Robert Zhang The University of Texas at Austin, The Johns Hopkins University Link to publication DOI Pre-print | ||
11:00 20mTalk | Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics OOPSLA 2024 Keith J.C. Johnson University of Wisconsin–Madison, Rahul Krishnan University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin-Madison DOI Pre-print | ||
11:20 20mTalk | HOL4P4: mechanized small-step semantics for P4 OOPSLA 2024 Anoud Alshnakat KTH Royal Institute of Technology, Didrik Lundberg KTH Royal Institute of Technology and Saab AB, Roberto Guanciale KTH Royal Institute of Technology, Mads Dam KTH DOI | ||
11:40 20mTalk | Semantics Lifting for Syntactic Sugar OOPSLA 2024 Zhichao Guan Peking University, Yiyuan Cao Peking University, Tailai Yu Tsinghua University, Ziheng Wang , Di Wang Peking University, Zhenjiang Hu Peking University DOI | ||
12:00 20mTalk | Synthesizing Formal Semantics from Executable Interpreters OOPSLA 2024 Jiangyi Liu University of Wisconsin - Madison, Charlie Murphy University of Wisconsin–Madison, Anvay Grover University of Wisconsin-Madison, Keith J.C. Johnson University of Wisconsin–Madison, Thomas Reps University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin-Madison DOI Pre-print |