Semantics Lifting for Syntactic Sugar

on YouTube ↗18m

" summary

Presents an algorithm that derives host-independent evaluation rules from host semantics and desugaring rules and implements it as Osazone, a tool that lifts semantics for syntactic sugar and generates interpreters. Proposes and proves four conditions (on syntactic sugars, meta-functions, and host semantics) that guarantee correctness and preservation of abstraction. Evaluates on seven benchmarks plus several real-world DSLs using lambda-calculus and mini-ML hosts, reports reproducible artifacts and that lifted semantics stays free of host constructs when conditions hold.

AI-written summary · about

" chapters (11)

1. 0:00Semantics lifting intro
2. 1:27Abstraction leakage in DSLs
3. 2:31Lifting vs typing challenges
4. 3:36Algorithm overview
5. 5:45Non-locality impact
6. 7:10Non-compositionality in rules
7. 8:16Preserving abstraction conditions
8. 10:26Implementation setup
9. 11:50Benchmark results
10. 12:33Summary and future
11. 13:15Q&A

" related talks

• 28mAdaptive Structural Operational SemanticsBenoit Combemale, Gwendal Jouneaux, Damian Frölich, Olivier Barais, Gurvan Le Guernic, Gunter Mussbacher, L. Thomas van Binsbergen · SLE 2023
• 40mFormal semantics for multi-language programsAmal Ahmed · PWLConf 2023
• 29mSemantic Transformation Framework for Rewriting RulesJihee Park, Sukyoung Ryu, Jaemin Hong · PEPM 2023
• 25mA Semantic Approach to Robust Property PreservationDerek Dreyer, Deepak Garg, Aina Linn Georges, Michael Sammler, Niklas Mück · PriSC 2025 (with POPL 2025)
• 20mCertified Abstract Machines for Skeletal SemanticsGuillaume Ambal, Serguei Lenglet, Alan Schmitt · CPP 2022
• 40mFormal semantics for multi-language programsAmal Ahmed · Strange Loop 2023
• 12mOn the power of syntactic methods: It is all syntax after all…Amr Sabry · TyDe 2022
• 31mProgramming Languages Must Have Formal Semantics. Period.Xiaohong Chen · RPLS 2025