OOPSLAB – Journal Issue

Artifacts Reusable Article: oopslab22main-p75-p doi:10.1145/3563288

First-Class Names for Effect Handlers
Ningning Xie, Youyou Cong, Kazuki Ikemori, and Daan Leijen
(University of Cambridge, UK; Tokyo Institute of Technology, Japan; Microsoft Research, USA)

Artifacts Reusable Article: oopslab22main-p88-p doi:10.1145/3563289

Compositional Virtual Timelines: Verifying Dynamic-Priority Partitions with Algorithmic Temporal Isolation
Mengqi Liu, Zhong Shao, Hao Chen, Man-Ki Yoon, and Jung-Eun Kim
(Yale University, USA)

Artifacts Functional Article: oopslab22main-p134-p doi:10.1145/3563290

Parsing Randomness
Harrison Goldstein and Benjamin C. Pierce
(University of Pennsylvania, USA)

Archive submitted (1.5 MB)

Artifacts Available Article: oopslab22main-p138-p doi:10.1145/3563291

CAAT: Consistency as a Theory
Thomas Haas, Roland Meyer, and Hernán Ponce de León
(TU Braunschweig, Germany; Huawei, Germany)

Artifacts Functional Article: oopslab22main-p182-p doi:10.1145/3563292

Reasoning about Distributed Reconfigurable Systems
Emma Ahrens, Marius Bozga, Radu Iosif, and Joost-Pieter Katoen
(RWTH Aachen University, Aachen, Germany; Université Grenoble Alpes, France; CNRS, France; Grenoble INP, France; VERIMAG, France)

Publisher's Version Article: oopslab22main-p191-p doi:10.1145/3563293

Compositional Embeddings of Domain-Specific Languages
Yaozhu Sun, Utkarsh Dhandhania, and Bruno C. d. S. Oliveira
(University of Hong Kong, China)

Archive submitted (930 kB)

Artifacts Reusable Article: oopslab22main-p196-p doi:10.1145/3563294

Scalable Linear Invariant Generation with Farkas’ Lemma
Hongming Liu, Hongfei Fu, Zhiyong Yu, Jiaxin Song, and Guoqiang Li
(Shanghai Jiao Tong University, China)

Artifacts Available Article: oopslab22main-p200-p doi:10.1145/3563295

Can Guided Decomposition Help End-Users Write Larger Block-Based Programs? A Mobile Robot Experiment
Nico Ritschel, Felipe Fronchetti, Reid Holmes, Ronald Garcia, and David C. Shepherd
(University of British Columbia, Canada; Virginia Commonwealth University, USA)

Publisher's Version Article: oopslab22main-p210-p doi:10.1145/3563296

Tower: Data Structures in Quantum Superposition
Charles Yuan and Michael Carbin
(Massachusetts Institute of Technology, USA)

Archive submitted (410 kB)

Artifacts Reusable Article: oopslab22main-p217-p doi:10.1145/3563297

Proving Hypersafety Compositionally
Emanuele D’Osualdo, Azadeh Farzan, and Derek Dreyer
(MPI-SWS, Germany; University of Toronto, Canada)

Publisher's Version Article: oopslab22main-p226-p doi:10.1145/3563298

Bridging the Semantic Gap between Qualitative and Quantitative Models of Distributed Systems
Si Liu, Jose Meseguer, Peter Csaba Ölveczky, Min Zhang, and David Basin
(ETH Zurich, Switzerland; University of Illinois at Urbana-Champaign, USA; University of Oslo, Norway; East China Normal University, China)

Artifacts Functional Article: oopslab22main-p234-p doi:10.1145/3563299

Concurrent Size
Gal Sela and Erez Petrank
(Technion, Israel)

Artifacts Reusable Article: oopslab22main-p237-p doi:10.1145/3563300

Wildcards Need Witness Protection
Kevin Bierhoff
(Google, USA)

Publisher's Version Article: oopslab22main-p240-p doi:10.1145/3563301

Overwatch: Learning Patterns in Code Edit Sequences
Yuhao Zhang, Yasharth Bajpai, Priyanshu Gupta, Ameya Ketkar, Miltiadis Allamanis, Titus Barik, Sumit Gulwani, Arjun Radhakrishna, Mohammad Raza, Gustavo Soares, and Ashish Tiwari
(University of Wisconsin-Madison, USA; Microsoft, India; Uber, USA; Microsoft Research, UK; Microsoft, USA)

Publisher's Version Article: oopslab22main-p242-p doi:10.1145/3563302

Incremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers
Aron Zwaan, Hendrik van Antwerpen, and Eelco Visser
(Delft University of Technology, Netherlands)

Archive submitted (1.2 MB)

Artifacts Functional Article: oopslab22main-p245-p doi:10.1145/3563303

MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types
Lionel Parreaux and Chun Yin Chau
(Hong Kong University of Science and Technology, China)

Artifacts Functional Article: oopslab22main-p248-p doi:10.1145/3563304

Highly Illogical, Kirk: Spotting Type Mismatches in the Large Despite Broken Contracts, Unsound Types, and Too Many Linters
Joshua Hoeflich, Robert Bruce Findler, and Manuel Serrano
(Northwestern University, USA; Inria, France; University of Côte d'Azur, France)

Publisher's Version Article: oopslab22main-p254-p doi:10.1145/3563305

Data-Driven Lemma Synthesis for Interactive Proofs
Aishwarya Sivaraman, Alex Sanchez-Stern, Bretton Chen, Sorin Lerner, and Todd Millstein
(University of California at Los Angeles, USA; University of Massachusetts at Amherst, USA; University of California at San Diego, USA)

Artifacts Functional Article: oopslab22main-p255-p doi:10.1145/3563306

Type-Directed Synthesis of Visualizations from Natural Language Queries
Qiaochu Chen, Shankara Pailoor, Celeste Barnaby, Abby Criswell, Chenglong Wang, Greg Durrett, and Işil Dillig
(University of Texas at Austin, USA; Microsoft Research, USA)

Publisher's Version Article: oopslab22main-p257-p doi:10.1145/3563307

Synthesis-Powered Optimization of Smart Contracts via Data Type Refactoring
Yanju Chen, Yuepeng Wang, Maruth Goyal, James Dong, Yu Feng, and Işil Dillig
(University of California at Santa Barbara, USA; Simon Fraser University, Canada; University of Texas at Austin, USA; Stanford University, USA)

Publisher's Version Article: oopslab22main-p261-p doi:10.1145/3563308

Verified Compilation of Quantum Oracles
Liyi Li, Finn Voichick, Kesha Hietala, Yuxiang Peng, Xiaodi Wu, and Michael Hicks
(University of Maryland, USA; Amazon, USA)

Artifacts Reusable Article: oopslab22main-p263-p doi:10.1145/3563309

Specification-Guided Component-Based Synthesis from Effectful Libraries
Ashish Mishra and Suresh Jagannathan
(Purdue University, USA)

Artifacts Available Article: oopslab22main-p266-p doi:10.1145/3563310

A Fast In-Place Interpreter for WebAssembly
Ben L. Titzer
(Carnegie Mellon University, USA)

Artifacts Reusable Article: oopslab22main-p273-p doi:10.1145/3563311

SigVM: Enabling Event-Driven Execution for Truly Decentralized Smart Contracts
Zihan Zhao, Sidi Mohamed Beillahi, Ryan Song, Yuxi Cai, Andreas Veneris, and Fan Long
(University of Toronto, Canada)

Artifacts Functional Article: oopslab22main-p281-p doi:10.1145/3563312

Solo: A Lightweight Static Analysis for Differential Privacy
Chiké Abuah, David Darais, and Joseph P. Near
(University of Vermont, USA; Galois, USA)

Artifacts Reusable Article: oopslab22main-p284-p doi:10.1145/3563313

A Conceptual Framework for Safe Object Initialization: A Principled and Mechanized Soundness Proof of the Celsius Model
Clément Blaudeau and Fengyun Liu
(Inria, France; Université de Paris-Cité, France; Oracle Labs, Switzerland)

Artifacts Reusable Article: oopslab22main-p289-p doi:10.1145/3563314

Model Checking for a Multi-Execution Memory Model
Evgenii Moiseenko, Michalis Kokologiannakis, and Viktor Vafeiadis
(JetBrains Research, Serbia; MPI-SWS, Germany)

Artifacts Reusable Article: oopslab22main-p296-p doi:10.1145/3563315

The Road Not Taken: Exploring Alias Analysis Based Optimizations Missed by the Compiler
Khushboo Chitre, Piyus Kedia, and Rahul Purandare
(IIIT Delhi, India; University of Nebraska-Lincoln, USA)

Artifacts Available Article: oopslab22main-p299-p doi:10.1145/3563316

Necessity Specifications for Robustness
Julian Mackay, Susan Eisenbach, James Noble, and Sophia Drossopoulou
(Victoria University of Wellington, New Zealand; Imperial College London, UK; Creative Research & Programming, New Zealand; Meta, UK)

Artifacts Functional Article: oopslab22main-p308-p doi:10.1145/3563317

A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
Dan Frumin, Emanuele D’Osualdo, Bas van den Heuvel, and Jorge A. Pérez
(University of Groningen, Netherlands; MPI-SWS, Germany)

Publisher's Version Article: oopslab22main-p325-p doi:10.1145/3563318

Coeffects for Sharing and Mutation
Riccardo Bianchini, Francesco Dagnino, Paola Giannini, Elena Zucca, and Marco Servetto
(University of Genoa, Italy; University of Eastern Piedmont, Italy; Victoria University of Wellington, New Zealand)

Publisher's Version Article: oopslab22main-p333-p doi:10.1145/3563319

The Essence of Online Data Processing
Philip Dexter, Yu David Liu, and Kenneth Chiu
(SUNY Binghamton, USA)

Artifacts Available Article: oopslab22main-p340-p doi:10.1145/3563320

Consistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
Zhihang Sun, Hongyu Fan, and Fei He
(Tsinghua University, China)

Publisher's Version Article: oopslab22main-p343-p doi:10.1145/3563321

Oracle-Free Repair Synthesis for Floating-Point Programs
Daming Zou, Yuchen Gu, Yuanfeng Shi, MingZhe Wang, Yingfei Xiong, and Zhendong Su
(ETH Zurich, Switzerland; Peking University, China; Princeton University, USA)

Publisher's Version Article: oopslab22main-p348-p doi:10.1145/3563322

Optimal Heap Limits for Reducing Browser Memory Use
Marisa Kirisame, Pranav Shenoy, and Pavel Panchekha
(University of Utah, USA)

Publisher's Version Article: oopslab22main-p349-p doi:10.1145/3563323

A General Construction for Abstract Interpretation of Higher-Order Automatic Differentiation
Jacob Laurel, Rem Yang, Shubham Ugare, Robert Nagel, Gagandeep Singh, and Sasa Misailovic
(University of Illinois at Urbana-Champaign, USA; VMware Research, USA)

Artifacts Functional Article: oopslab22main-p350-p doi:10.1145/3563324

Scalable Verification of GNN-Based Job Schedulers
Haoze Wu, Clark Barrett, Mahmood Sharif, Nina Narodytska, and Gagandeep Singh
(Stanford University, USA; Tel Aviv University, Israel; VMware Research, USA; University of Illinois at Urbana-Champaign, USA)

Artifacts Available Article: oopslab22main-p353-p doi:10.1145/3563325

Fractional Resources in Unbounded Separation Logic
Thibault Dardinier, Peter Müller, and Alexander J. Summers
(ETH Zurich, Switzerland; University of British Columbia, Canada)

Artifacts Reusable Article: oopslab22main-p356-p doi:10.1145/3563326

Neurosymbolic Repair for Low-Code Formula Languages
Rohan Bavishi, Harshit Joshi, José Cambronero, Anna Fariha, Sumit Gulwani, Vu Le, Ivan Radiček, and Ashish Tiwari
(University of California at Berkeley, USA; Microsoft, India; Microsoft, USA; Microsoft, Croatia)

Archive submitted (350 kB) Article: oopslab22main-p370-p doi:10.1145/3563327

A Study of Inline Assembly in Solidity Smart Contracts
Stefanos Chaliasos, Arthur Gervais, and Benjamin Livshits
(Imperial College London, UK)

Artifacts Reusable Article: oopslab22main-p379-p doi:10.1145/3563328

Neural Architecture Search using Property Guided Synthesis
Charles Jin, Phitchaya Mangpo Phothilimthana, and Sudip Roy
(Massachusetts Institute of Technology, USA; Google Research, USA; Cohere, USA)

Archive submitted (1.3 MB) Article: oopslab22main-p383-p doi:10.1145/3563329

Seq2Parse: Neurosymbolic Parse Error Repair
Georgios Sakkas, Madeline Endres, Philip J. Guo, Westley Weimer, and Ranjit Jhala
(University of California at San Diego, USA; University of Michigan, USA)

Artifacts Functional Article: oopslab22main-p391-p doi:10.1145/3563330

Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid
Stephen Ellis, Shuofei Zhu, Nobuko Yoshida, and Linhai Song
(University of Oxford, UK; Pennsylvania State University, USA)

Artifacts Functional Article: oopslab22main-p418-p doi:10.1145/3563331

Satisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
Sujit Kumar Muduli and Subhajit Roy
(IIT Kanpur, India)

Artifacts Reusable Article: oopslab22main-p420-p doi:10.1145/3563332

UniRec: A Unimodular-Like Framework for Nested Recursions and Loops
Kirshanthan Sundararajah, Charitha Saumya, and Milind Kulkarni
(Purdue University, USA)

Publisher's Version Article: oopslab22main-p423-p doi:10.1145/3563333

Synthesizing Abstract Transformers
Pankaj Kumar Kalita, Sujit Kumar Muduli, Loris D’Antoni, Thomas Reps, and Subhajit Roy
(IIT Kanpur, India; University of Wisconsin-Madison, USA)

Artifacts Functional Article: oopslab22main-p436-p doi:10.1145/3563334

Monadic and Comonadic Aspects of Dependency Analysis
Pritam Choudhury
(University of Pennsylvania, USA)

Publisher's Version Article: oopslab22main-p437-p doi:10.1145/3563335

Katara: Synthesizing CRDTs with Verified Lifting
Shadaj Laddad, Conor Power, Mae Milano, Alvin Cheung, and Joseph M. Hellerstein
(University of California at Berkeley, USA)

Artifacts Functional Article: oopslab22main-p454-p doi:10.1145/3563336

A Concurrent Program Logic with a Future and History
Roland Meyer, Thomas Wies, and Sebastian Wolff
(TU Braunschweig, Germany; New York University, USA)

Artifacts Reusable Article: oopslab22main-p465-p doi:10.1145/3563337

Compilation of Dynamic Sparse Tensor Algebra
Stephen Chou and Saman Amarasinghe
(Massachusetts Institute of Technology, USA)

Artifacts Functional Article: oopslab22main-p477-p doi:10.1145/3563338

Indexing the Extended Dyck-CFL Reachability for Context-Sensitive Program Analysis
Qingkai Shi, Yongchao Wang, Peisen Yao, and Charles Zhang
(Ant Group, China; Hong Kong University of Science and Technology, China)

Publisher's Version Article: oopslab22main-p486-p doi:10.1145/3563339

Checking Equivalence in a Non-strict Language
John C. Kolesar, Ruzica Piskac, and William T. Hallahan
(Yale University, USA; Binghamton University, USA)

Artifacts Functional Article: oopslab22main-p495-p doi:10.1145/3563340

This Is the Moment for Probabilistic Loops
Marcel Moosbrugger, Miroslav Stankovič, Ezio Bartocci, and Laura Kovács
(TU Wien, Austria)

Artifacts Reusable Article: oopslab22main-p505-p doi:10.1145/3563341

A case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning
Aleksander Boruch-Gruszecki, Radosław Waśko, Yichen Xu, and Lionel Parreaux
(EPFL, Switzerland; University of Warsaw, Poland; Beijing University of Posts and Telecommunications, China; Hong Kong University of Science and Technology, China)

Artifacts Reusable Article: oopslab22main-p508-p doi:10.1145/3563342

Taming Transitive Redundancy for Context-Free Language Reachability
Yuxiang Lei, Yulei Sui, Shuo Ding, and Qirun Zhang
(University of Technology Sydney, Australia; Georgia Institute of Technology, USA)

Artifacts Reusable Article: oopslab22main-p513-p doi:10.1145/3563343

Symbolic Execution for Randomized Programs
Zachary Susag, Sumit Lahiri, Justin Hsu, and Subhajit Roy
(Cornell University, USA; IIT Kanpur, India)

Artifacts Functional Article: oopslab22main-p535-p doi:10.1145/3563344

BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs
Fengmin Zhu, Michael Sammler, Rodolphe Lepigre, Derek Dreyer, and Deepak Garg
(MPI-SWS, Germany)

Artifacts Reusable Article: oopslab22main-p545-p doi:10.1145/3563345

High-Level Effect Handlers in C++
Dan Ghica, Sam Lindley, Marcos Maroñas Bravo, and Maciej Piróg
(Huawei, UK; University of Edinburgh, UK)

Artifacts Reusable Article: oopslab22main-p561-p doi:10.1145/3563445

Semi-symbolic Inference for Efficient Streaming Probabilistic Programming
Eric Atkinson, Charles Yuan, Guillaume Baudart, Louis Mandel, and Michael Carbin
(Massachusetts Institute of Technology, USA; ENS — PSL University — CNRS — Inria, France; IBM Research, USA)

Artifacts Reusable Article: oopslab22main-p566-p doi:10.1145/3563347

Synthesizing Axiomatizations using Logic Learning
Paul Krogmeier, Zhengyao Lin, Adithya Murali, and P. Madhusudan
(University of Illinois at Urbana-Champaign, USA)

Artifacts Available Article: oopslab22main-p588-p doi:10.1145/3563348

Veracity: Declarative Multicore Programming with Commutativity
Adam Chen, Parisa Fathololumi, Eric Koskinen, and Jared Pincus
(Stevens Institute of Technology, USA)

Artifacts Reusable Article: oopslab22main-p594-p doi:10.1145/3563349

Synthesizing Code Quality Rules from Examples
Pranav Garg and Srinivasan H. Sengamedu
(AWS, USA; Amazon, USA)

Archive submitted (1.2 MB) Article: oopslab22main-p602-p doi:10.1145/3563350

Modular Verification of Op-Based CRDTs in Separation Logic
Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, and Lars Birkedal
(Aarhus University, Denmark; ENS Lyon, France)

Artifacts Reusable Article: oopslab22main-p641-p doi:10.1145/3563351

Implementing and Verifying Release-Acquire Transactional Memory in C11
Sadegh Dalvandi and Brijesh Dongol
(University of Surrey, UK)

Artifacts Available Article: oopslab22main-p648-p doi:10.1145/3563352

Fast Shadow Execution for Debugging Numerical Errors using Error Free Transformations
Sangeeta Chowdhary and Santosh Nagarakatte
(Rutgers University, USA)

Artifacts Functional Article: oopslab22main-p662-p doi:10.1145/3563353

Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints
Adithya Murali, Lucas Peña, Eion Blanchard, Christof Löding, and P. Madhusudan
(University of Illinois at Urbana-Champaign, USA; RWTH Aachen University, Germany)

Artifacts Available Article: oopslab22main-p769-p doi:10.1145/3563354

Intrinsically-Typed Definitional Interpreters à la Carte
Cas van der Rest, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser, and Peter Mosses
(Delft University of Technology, Netherlands)