One Down, 699 to Go: or, Synthesising Compositional DesugaringsVirtual
Fri 22 Oct 2021 19:20 - 19:35 at Zurich D - Synthesis of models, tools and programs -- mirror Chair(s): Alex Potanin
Programming or scripting languages used in real-world systems are seldom designed with a formal semantics in mind from the outset. Therefore, developing well-founded analysis tools for these systems requires reverse-engineering a formal semantics as a first step. This can take months or years of effort.
Can we (at least partially) automate this process? Though desirable, automatically reverse-engineering semantics rules from an implementation is very challenging, as found by Krishnamurthi, Lerner and Elberty. In this paper, we highlight that scaling methods with the size of the language is very difficult due to state space explosion, so we propose to learn semantics incrementally. We give a formalisation of Krishnamurthi et al.'s desugaring learning framework in order to clarify the assumptions necessary for an incremental learning algorithm to be feasible.
We show that this reformulation allows us to extend the search space and express rules that Krishnamurthi et al. described as challenging, while still retaining feasibility. We evaluate enumerative synthesis as a baseline algorithm, and demonstrate that, with our reformulation of the problem, it is possible to learn correct desugaring rules for the example source and core languages proposed by Krishnamurthi et al., in most cases identical to the intended rules. In addition, with user guidance, our system was able to synthesize rules for desugaring list comprehensions and try/catch/finally constructs.
Fri 22 OctDisplayed time zone: Central Time (US & Canada) change
10:50 - 12:10 | Synthesis of models, tools and programsOOPSLA at Zurich D +8h Chair(s): Jonathan Aldrich Carnegie Mellon University | ||
10:50 15mTalk | Rewrite Rule Inference Using Equality SaturationVirtual OOPSLA Chandrakana Nandi Certora, inc., Max Willsey University of Washington, Amy Zhu University of Washington, Yisu Remy Wang University of Washington, Brett Saiki University of Washington, Adam Anderson University of Washington, Adriana Schulz University of Washington, Dan Grossman University of Washington, Zachary Tatlock University of Washington DOI | ||
11:05 15mTalk | Semantic Programming by Example with Pre-trained ModelsVirtual OOPSLA DOI | ||
11:20 15mTalk | One Down, 699 to Go: or, Synthesising Compositional DesugaringsVirtual OOPSLA Sándor Bartha University of Edinburgh, James Cheney University of Edinburgh; Alan Turing Institute, Vaishak Belle University of Edinburgh; Alan Turing Institute DOI | ||
11:35 15mTalk | Multi-modal Program Inference: A Marriage of Pre-trained Language Models and Component-Based SynthesisIn-Person OOPSLA Kia Rahmani Purdue University, Mohammad Raza Microsoft, Sumit Gulwani Microsoft, Vu Le Microsoft, Daniel Morris Microsoft, Arjun Radhakrishna Microsoft, Gustavo Soares Microsoft, Ashish Tiwari Microsoft DOI Pre-print | ||
11:50 20mLive Q&A | Discussion, Questions and Answers OOPSLA |
18:50 - 20:10 | Synthesis of models, tools and programs -- mirrorOOPSLA at Zurich D Chair(s): Alex Potanin Victoria University of Wellington | ||
18:50 15mTalk | Rewrite Rule Inference Using Equality SaturationVirtual OOPSLA Chandrakana Nandi Certora, inc., Max Willsey University of Washington, Amy Zhu University of Washington, Yisu Remy Wang University of Washington, Brett Saiki University of Washington, Adam Anderson University of Washington, Adriana Schulz University of Washington, Dan Grossman University of Washington, Zachary Tatlock University of Washington DOI | ||
19:05 15mTalk | Semantic Programming by Example with Pre-trained ModelsVirtual OOPSLA DOI | ||
19:20 15mTalk | One Down, 699 to Go: or, Synthesising Compositional DesugaringsVirtual OOPSLA Sándor Bartha University of Edinburgh, James Cheney University of Edinburgh; Alan Turing Institute, Vaishak Belle University of Edinburgh; Alan Turing Institute DOI | ||
19:35 15mTalk | Multi-modal Program Inference: A Marriage of Pre-trained Language Models and Component-Based SynthesisIn-Person OOPSLA Kia Rahmani Purdue University, Mohammad Raza Microsoft, Sumit Gulwani Microsoft, Vu Le Microsoft, Daniel Morris Microsoft, Arjun Radhakrishna Microsoft, Gustavo Soares Microsoft, Ashish Tiwari Microsoft DOI Pre-print | ||
19:50 20mLive Q&A | Discussion, Questions and Answers OOPSLA |