Wed 23 Oct 2024 11:40 - 12:00 at San Gabriel - Semantics Chair(s): Ilya Sergey

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 Oct

Displayed time zone: Pacific Time (US & Canada) change

10:40 - 12:20
SemanticsOOPSLA 2024 at San Gabriel
Chair(s): Ilya Sergey National University of Singapore
10:40
20m
Talk
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
20m
Talk
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
20m
Talk
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
20m
Talk
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
20m
Talk
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