SPLASH 2023 - OOPSLA - SPLASH 2023

Time Zone

The program is currently displayed in (GMT+01:00) Lisbon.

Use conference time zone: (GMT+01:00) LisbonSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

You're viewing the program in a time zone which is different from your device's time zone change time zone

Wed 25 Oct
Displayed time zone: Lisbon change

09:00 - 09:30	Opening and WelcomeOOPSLA at Room I Chair(s): Vasco T. Vasconcelos LASIGE, University of Lisbon Welcome to SPLASH OOPSLA Review Committee Board report, including Distinguished OOPSLA 2023 papers

09:00 30m Other		Opening and Welcome OOPSLA

09:30 - 10:30	Keynote 1OOPSLA at Room I

09:30 60m Keynote		Scaling up machine learning without tears (and what do programming languages have to do with it)Keynote OOPSLA Dimitrios Vytiniotis Google DeepMind

	10:30 - 11:00	Coffee BreakCatering at Gallery

11:00 - 12:30	AI4SEOOPSLA at Room I Chair(s): Guido Salvaneschi University of St. Gallen

11:00 18m Talk		Grounded Copilot: How Programmers Interact with Code-Generating Models OOPSLA Shraddha Barke University of California at San Diego, Michael B. James University of California at San Diego, Nadia Polikarpova University of California at San Diego DOI
11:18 18m Talk		Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs OOPSLA Alex Renda Massachusetts Institute of Technology, Yi Ding Purdue University, Michael Carbin Massachusetts Institute of Technology DOI Pre-print
11:36 18m Talk		Concrete Type Inference for Code Optimization using Machine Learning with SMT Solving OOPSLA Fangke Ye Georgia Institute of Technology, Jisheng Zhao Georgia Institute of Technology, Jun Shirako Georgia Institute of Technology, Vivek Sarkar Georgia Institute of Technology DOI
11:54 18m Talk		An Explanation Method for Models of Code OOPSLA Yu Wang Nanjing University, Ke Wang , Linzhang Wang Nanjing University DOI
12:12 18m Talk		Optimization-Aware Compiler-Level Event Profiling OOPSLA Matteo Basso Università della Svizzera italiana (USI), Switzerland, Aleksandar Prokopec Oracle Labs, Andrea Rosà USI Lugano, Walter Binder USI Lugano Link to publication DOI

11:00 - 12:30	program synthesis 1OOPSLA at Room II Chair(s): Michael Coblenz University of California, San Diego

11:00 18m Talk		Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart Contracts OOPSLA Zhuo Cai Hong Kong University of Science and Technology, Soroush Farokhnia Hong Kong University of Science and Technology, Amir Kafshdar Goharshady Hong Kong University of Science and Technology, S. Hitarth Hong Kong University of Science and Technology DOI
11:18 18m Talk		Equality Saturation Theory Exploration à la Carte OOPSLA Anjali Pal University of Washington, Brett Saiki University of Washington, Ryan Tjoa University of Washington, Cynthia Richey University of Washington, Amy Zhu University of Washington, Oliver Flatt University of Washington, Max Willsey UC Berkeley, Zachary Tatlock University of Washington, Chandrakana Nandi Certora DOI Pre-print
11:36 18m Talk		Synthesizing Specifications OOPSLA Kanghee Park University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison DOI
11:54 18m Talk		Explainable Program Synthesis by Localizing Specifications OOPSLA Amirmohammad Nazari University of Southern California, Yifei Huang University of Southern California, Roopsha Samanta Purdue University, Arjun Radhakrishna Microsoft, Mukund Raghothaman University of Southern California DOI
12:12 18m Talk		Pushing the Limit of 1-Minimality of Language-Agnostic Program Reduction OOPSLA Zhenyang Xu University of Waterloo, Yongqiang Tian The Hong Kong University of Science and Technology; University of Waterloo, Mengxiao Zhang University of Waterloo, Gaosen Zhao University of Waterloo, Yu Jiang Tsinghua University, Chengnian Sun University of Waterloo DOI

	12:30 - 14:00	LunchCatering at Gallery

14:00 - 15:30	SE4AIOOPSLA at Room I Chair(s): Arjun Guha Northeastern University; Roblox

14:00 18m Talk		Run-Time Prevention of Software Integration Failures of Machine Learning APIs OOPSLA Chengcheng Wan East China Normal University, Yuhan Liu University of Chicago, Kuntai Du University of Chicago, Henry Hoffmann University of Chicago, Junchen Jiang University of Chicago, Michael Maire University of Chicago, Shan Lu Microsoft; University of Chicago DOI
14:18 18m Talk		Compiling Structured Tensor Algebra OOPSLA Mahdi Ghorbani University of Edinburgh, Mathieu Huot University of Oxford, Shideh Hashemian University of Edinburgh, Amir Shaikhha University of Edinburgh DOI
14:36 18m Talk		Perception Contracts for Safety of ML-Enabled Systems OOPSLA Angello Astorga University of Illinois at Urbana-Champaign, Chiao Hsieh Kyoto University, P. Madhusudan University of Illinois at Urbana-Champaign, Sayan Mitra University of Illinois at Urbana-Champaign DOI
14:54 18m Talk		Languages with Decidable Learning: A Meta-theorem OOPSLA Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign DOI
15:12 18m Talk		Deep Learning Robustness Verification for Few-Pixel Attacks OOPSLA Yuval Shapira Technion, Eran Avneri Technion, Dana Drachsler Cohen Technion DOI

14:00 - 15:30	program synthesis 2OOPSLA at Room II Chair(s): Chandrakana Nandi Certora

14:00 18m Talk		Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates OOPSLA Aalok Thakkar University of Pennsylvania, Nathaniel Sands University of Southern California, Georgios Petrou University of Southern California, Rajeev Alur University of Pennsylvania, Mayur Naik University of Pennsylvania, Mukund Raghothaman University of Southern California DOI
14:18 18m Talk		Data Extraction via Semantic Regular Expression Synthesis OOPSLA Jocelyn (Qiaochu) Chen University of Texas at Austin, Arko Banerjee University of Texas at Austin, Çağatay Demiralp Massachusetts Institute of Technology, Greg Durrett University of Texas at Austin, Işıl Dillig University of Texas at Austin DOI
14:36 18m Talk		Synthesizing Efficient Memoization Algorithms OOPSLA Yican Sun Peking University, Xuanyu Peng Peking University, Yingfei Xiong Peking University DOI
14:54 18m Talk		Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs OOPSLA Amir Kafshdar Goharshady Hong Kong University of Science and Technology, S. Hitarth Hong Kong University of Science and Technology, Fatemeh Mohammadi KU Leuven, Harshit Jitendra Motwani Ghent University DOI
15:12 18m Talk		Modular Component-Based Quantum Circuit Synthesis OOPSLA Chan Gu Kang Korea University, Hakjoo Oh Korea University DOI

	15:30 - 16:00	Coffee BreakCatering at Gallery

16:00 - 17:30	probabilisticOOPSLA at Room I Chair(s): Chandrakana Nandi Certora

16:00 18m Talk		A Deductive Verification Infrastructure for Probabilistic Programs OOPSLA Philipp Schröer RWTH Aachen University, Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU DOI
16:18 18m Talk		A Gradual Probabilistic Lambda Calculus OOPSLA Wenjia Ye University of Hong Kong, Matías Toro University of Chile, Federico Olmedo University of Chile DOI
16:36 18m Talk		Lower Bounds for Possibly Divergent Probabilistic Programs OOPSLA Shenghua Feng Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Mingshuai Chen Zhejiang University, Han Su Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Naijun Zhan Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences Link to publication DOI Pre-print
16:54 18m Talk		Exact Recursive Probabilistic Programming OOPSLA David Chiang University of Notre Dame, Colin McDonald University of Notre Dame, Chung-chieh Shan Indiana University DOI
17:12 18m Talk		Solving String Constraints with Lengths by Stabilization OOPSLA Yu-Fang Chen Academia Sinica, David Chocholatý Brno University of Technology, Vojtěch Havlena Brno University of Technology, Lukáš Holík Brno University of Technology, Ondřej Lengál Brno University of Technology, Juraj Síč Brno University of Technology DOI

16:00 - 17:48	DSLsOOPSLA at Room II Chair(s): Ben Greenman Brown University, USA

16:00 18m Talk		Fluent APIs in Functional Languages OOPSLA Ori Roth Technion, Yossi Gil Technion DOI Pre-print
16:18 18m Talk		A Pretty Expressive Printer OOPSLA Sorawee Porncharoenwase University of Washington, Justin Pombrio Unaffiliated, Emina Torlak Amazon Web Services, USA DOI Pre-print
16:36 18m Talk		How Domain Experts Use an Embedded DSL OOPSLA Lisa Rennels University of California at Berkeley, Sarah E. Chasins University of California at Berkeley DOI
16:54 18m Talk		Saggitarius: A DSL for Specifying Grammatical Domains OOPSLA Anders Miltner Simon Fraser University, Devon Loehr Princeton University, Arnold Mong Princeton University, Kathleen Fisher Tufts University, David Walker Princeton University DOI
17:12 18m Talk		Mat2Stencil: A Modular Matrix-Based DSL for Explicit and Implicit Matrix-Free PDE Solvers on Structured Grid OOPSLA Huanqi Cao Tsinghua University, Shizhi Tang Tsinghua University, Qianchao Zhu Peking University, Bowen Yu Tsinghua University, Wenguang Chen Tsinghua University; Pengcheng Laboratory DOI
17:30 18m Talk		Translating canonical SQL to imperative code in Coq OOPSLA Véronique Benzaken Université Paris-Saclay - Laboratoire de Méthodes Formelles , Évelyne Contejean CNRS, ENS Paris-Saclay & Université Paris-Saclay, Houssem Hachmaoui , Chantal Keller Université Paris Saclay, Louis Mandel IBM Research, USA, Avraham Shinnar IBM Research, Jerome Simeon DocuSign, Inc. Link to publication DOI

17:45 - 19:30	ReceptionCatering at Gallery

17:45 1h45m Dinner		Reception Catering

Thu 26 Oct
Displayed time zone: Lisbon change

09:30 - 10:30	Keynote 2OOPSLA at Room I Chair(s): Mira Mezini TU Darmstadt

09:30 60m Keynote		Hydroflow: A Compiler Target for Fast, Correct Distributed ProgramsKeynote OOPSLA Joseph M. Hellerstein UC Berkeley

	10:30 - 11:00	Coffee BreakCatering at Gallery

11:00 - 12:30	type systems 1OOPSLA at Room I Chair(s): Max S. New University of Michigan

11:00 18m Talk		Reference Capabilities for Flexible Memory Management OOPSLA Ellen Arvidsson Uppsala University, Elias Castegren Uppsala University, Sylvan Clebsch Microsoft Azure Research, Sophia Drossopoulou Imperial College London, James Noble Research & Programming, Matthew J. Parkinson Microsoft Azure Research, Tobias Wrigstad Uppsala University DOI Pre-print
11:18 18m Talk		A Grounded Conceptual Model for Ownership Types in Rust OOPSLA Will Crichton Brown University, Gavin Gray ETH Zurich, Shriram Krishnamurthi Brown University DOI Pre-print
11:36 18m Talk		Inference of Resource Management Specifications OOPSLA Narges Shadab University of California at Riverside, Pritam Gharat Microsoft Research, Shrey Tiwari Microsoft Research, Michael D. Ernst University of Washington, Martin Kellogg New Jersey Institute of Technology, Shuvendu K. Lahiri Microsoft Research, Akash Lal Microsoft Research, Manu Sridharan University of California at Riverside DOI
11:54 18m Talk		Resource-Aware Soundness for Big-Step Semantics OOPSLA Riccardo Bianchini University of Genoa, Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa DOI
12:12 18m Talk		Verus: Verifying Rust Programs using Linear Ghost Types OOPSLA Andrea Lattuada VMware Research, Travis Hance Carnegie Mellon University, Chanhee Cho Carnegie Mellon University, Matthias Brun ETH Zurich, Isitha Subasinghe UNSW Sydney, Yi Zhou Carnegie Mellon University, Jon Howell VMware Research, Bryan Parno Carnegie Mellon University, Chris Hawblitzel Microsoft Research DOI

11:00 - 12:30	language semanticsOOPSLA at Room II Chair(s): Sebastian Erdweg JGU Mainz

11:00 18m Talk		The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog OOPSLA Qinlin Chen Nanjing University, Nairen Zhang Nanjing University, Jinpeng Wang Nanjing University, Tian Tan Nanjing University, Chang Xu Nanjing University, Xiaoxing Ma Nanjing University, Yue Li Nanjing University DOI
11:18 18m Talk		Regular Expression Matching using Bit Vector Automata OOPSLA Alexis Le Glaunec Rice University, Lingkun Kong Rice University, Konstantinos Mamouras Rice University DOI
11:36 18m Talk		Bidirectional Object-Oriented Programming: Towards Programmatic and Direct Manipulation of Objects OOPSLA Xing Zhang Peking University, Guanchen Guo Peking University, Xiao He University of Science and Technology Beijing, Zhenjiang Hu Peking University DOI
11:54 18m Talk		Bring Your Own Data Structures to Datalog OOPSLA Arash Sahebolamri Syracuse University, Langston Barrett Galois, Scott Moore Galois, Kristopher Micinski Syracuse University DOI
12:12 18m Talk		Rhombus: A New Spin on Macros without All the Parentheses OOPSLA Matthew Flatt University of Utah, Taylor Allred University of Utah, Nia Angle independent, Stephen De Gabrielle independent, Robert Bruce Findler Northwestern University, Jack Firth independent, Kiran Gopinathan National University of Singapore, Ben Greenman University of Utah, Siddhartha Kasivajhula independent, Alex Knauth independent, Jay McCarthy Reach, Sam Phillips independent, Sorawee Porncharoenwase University of Washington, Jens Axel Søgaard independent, Sam Tobin-Hochstadt Indiana University DOI Pre-print

	12:30 - 14:00	LunchCatering at Gallery

14:00 - 15:30	type systems 2OOPSLA at Room I Chair(s): Max S. New University of Michigan

14:00 18m Talk		Greedy Implicit Bounded Quantification OOPSLA Chen Cui University of Hong Kong, Shengyi Jiang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI
14:18 18m Talk		Structural Subtyping as Parametric Polymorphism OOPSLA Wenhao Tang University of Edinburgh, Daniel Hillerström Huawei Zurich Research Center, James McKinna Heriot-Watt University, Michel Steuwer TU Berlin; University of Edinburgh, Ornela Dardha University of Glasgow, Rongxiao Fu University of Edinburgh, Sam Lindley University of Edinburgh DOI Pre-print
14:36 18m Talk		Simple Reference Immutability for System F<: OOPSLA Edward Lee University of Waterloo, Ondřej Lhoták University of Waterloo DOI
14:54 18m Talk		Mutually Iso-Recursive Subtyping OOPSLA Andreas Rossberg Independent DOI
15:12 18m Talk		Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference OOPSLA Ishan Bhanuka Hong Kong University of Science and Technology, Lionel Parreaux Hong Kong University of Science and Technology, David Binder University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen DOI Pre-print

14:00 - 15:30	program analysis 1OOPSLA at Room II Chair(s): Manu Sridharan University of California at Riverside

14:00 18m Talk		The Bounded Pathwidth of Control-Flow Graphs OOPSLA Giovanna Kobus Conrado Hong Kong University of Science and Technology, Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Chun Kit Lam Hong Kong University of Science and Technology DOI
14:18 18m Talk		How Profilers Can Help Navigate Type Migration OOPSLA Ben Greenman University of Utah, Matthias Felleisen Northeastern University, Christos Dimoulas Northwestern University DOI
14:36 18m Talk		Synthesizing Precise Static Analyzers for Automatic Differentiation OOPSLA Jacob Laurel University of Illinois at Urbana-Champaign, Siyuan Brant Qian University of Illinois at Urbana-Champaign; Zhejiang University, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research, Sasa Misailovic University of Illinois at Urbana-Champaign DOI
14:54 18m Talk		A Container-Usage-Pattern-Based Context Debloating Approach for Object-Sensitive Pointer Analysis OOPSLA Dongjie He UNSW, Yujiang Gui UNSW, Wei Li UNSW, Yonggang Tao UNSW, Changwei Zou UNSW, Yulei Sui UNSW, Jingling Xue UNSW DOI Pre-print
15:12 18m Talk		Static Analysis of Memory Models for SMT Encodings OOPSLA Thomas Haas TU Braunschweig, René Maseli TU Braunschweig, Roland Meyer TU Braunschweig, Hernán Ponce de León Huawei DOI

	15:30 - 16:00	Coffee BreakCatering at Gallery

16:00 - 17:30	effect systemsOOPSLA at Room I Chair(s): Sebastian Erdweg JGU Mainz

16:00 18m Talk		Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems OOPSLA Magnus Madsen Aarhus University, Jaco van de Pol Aarhus University, Troels Henriksen University of Copenhagen DOI
16:18 18m Talk		From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers OOPSLA Marius Müller University of Tübingen, Philipp Schuster University of Tübingen, Jonathan Lindegaard Starup Aarhus University, Klaus Ostermann University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen Link to publication DOI Pre-print
16:36 18m Talk		Gradual Typing for Effect Handlers OOPSLA Max S. New University of Michigan, Eric Giovannini University of Michigan, Daniel R. Licata Wesleyan University DOI
16:54 18m Talk		When Concurrency Matters: Behaviour-Oriented Concurrency OOPSLA Luke Cheeseman Imperial College London, Matthew J. Parkinson Microsoft Azure Research, Sylvan Clebsch Microsoft Azure Research, Marios Kogias Imperial College London; Microsoft Research, Sophia Drossopoulou Imperial College London, David Chisnall Microsoft, Tobias Wrigstad Uppsala University, Paul Liétar Imperial College London DOI
17:12 18m Talk		Continuing WebAssembly with Effect Handlers OOPSLA Luna Phipps-Costin Northeastern University, Andreas Rossberg Independent, Arjun Guha Northeastern University; Roblox, Daan Leijen Microsoft Research, Daniel Hillerström Huawei Zurich Research Center, KC Sivaramakrishnan Tarides; IIT Madras, Matija Pretnar University of Ljubljana, Sam Lindley University of Edinburgh DOI Pre-print

16:00 - 17:30	program analysis 2OOPSLA at Room II Chair(s): Annette Bieniusa University of Kaiserslautern-Landau

16:00 18m Talk		Historia: Refuting Callback Reachability with Message-History Logics OOPSLA Shawn Meier University of Colorado at Boulder, Sergio Mover École Polytechnique, Gowtham Kaki University of Colorado at Boulder, Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon DOI
16:18 18m Talk		Exploiting the Sparseness of Control-Flow and Call Graphs for Efficient and On-Demand Algebraic Program Analysis OOPSLA Giovanna Kobus Conrado Hong Kong University of Science and Technology, Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Kerim Kochekov Hong Kong University of Science and Technology, Yun Chen Tsai Hong Kong University of Science and Technology, Ahmed Khaled Zaher Hong Kong University of Science and Technology DOI
16:36 18m Talk		A Cocktail Approach to Practical Call Graph Construction OOPSLA Yuandao Cai Hong Kong University of Science and Technology, Charles Zhang Hong Kong University of Science and Technology DOI
16:54 18m Talk		Building Dynamic System Call Sandbox with Partial Order Analysis OOPSLA Quan Zhang Tsinghua University, Chijin Zhou Tsinghua University, Yiwen Xu Tsinghua University, Zijing Yin Tsinghua University, Mingzhe Wang Tsinghua University, Zhuo Su Tsinghua University, Chengnian Sun University of Waterloo, Yu Jiang Tsinghua University, Jiaguang Sun Tsinghua University DOI
17:12 18m Talk		Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection OOPSLA Ruyi Ji Peking University, Chaozhe Kong Peking University, Yingfei Xiong Peking University, Zhenjiang Hu Peking University DOI

16:00 - 17:30	compilation & optimization 2OOPSLA at Room XII Chair(s): Fabian Muehlboeck Australian National University

16:00 18m Talk		Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies OOPSLA Oliver Bračevac Galois, Inc., Guannan Wei Purdue University, Songlin Jia Purdue University, Supun Abeysinghe Purdue University, Yuxuan Jiang Purdue University, Yuyan Bao Augusta University, Tiark Rompf Purdue University DOI Pre-print
16:18 18m Talk		AST vs. Bytecode: Interpreters in the Age of Meta-Compilation OOPSLA Octave Larose University of Kent, Sophie Kaleba University of Kent, Humphrey Burchell University of Kent, Stefan Marr University of Kent DOI Pre-print
16:36 18m Talk		Reusing Just-in-Time Compiled Code OOPSLA Meetesh Kalpesh Mehta IIT Bombay, Sebastián Krynski Czech Technical University in Prague, Hugo Musso Gualandi Czech Technical University in Prague, Manas Thakur IIT Bombay, Jan Vitek Northeastern University DOI
16:54 18m Talk		TASTyTruffle: Just-in-Time Specialization of Parametric Polymorphism OOPSLA Matt D'Souza University of Waterloo, James You University of Waterloo, Ondřej Lhoták University of Waterloo, Aleksandar Prokopec Oracle Labs DOI
17:12 18m Talk		Beacons: An End-to-End Compiler Framework for Predicting and Utilizing Dynamic Loop Characteristics OOPSLA Girish Mururu Georgia Institute of Technology, Sharjeel Khan Georgia Institute of Technology, Bodhisatwa Chatterjee Georgia Institute of Technology, Chao Chen Georgia Institute of Technology, Chris Porter IBM T.J. Watson Research, Ada Gavrilovska Georgia Institute of Technology, Santosh Pande Georgia Institute of Technology DOI

17:30 - 17:45	Sponsored TalksSponsored Talks at Room I Chair(s): Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon

17:30 15m Talk		Programming Languages at Huawei Sponsored Talks A: Dan Ghica Huawei

Fri 27 Oct
Displayed time zone: Lisbon change

	09:00 - 09:30	AnnouncementsOOPSLA at Room I Chair(s): Vasco T. Vasconcelos LASIGE, University of Lisbon Most Influential Paper Award Student Research Competition Award Artifact Evaluation Chair Report, including Distinguished OOPSLA Artifacts and Distinguished AEC Reviewers SPLASH 2024 Pitch

09:30 - 10:30	Keynote 3OOPSLA at Room I Chair(s): Mira Mezini TU Darmstadt

09:30 60m Keynote		All the Languages TogetherKeynote OOPSLA Amal Ahmed Northeastern University, USA

	10:30 - 11:00	Coffee BreakCatering at Gallery

11:00 - 12:30	verification 1OOPSLA at Room I Chair(s): Gowtham Kaki University of Colorado at Boulder

11:00 18m Talk		Solving Conditional Linear Recurrences for Program Verification: The Periodic Case OOPSLA Chenglin Wang Hong Kong University of Science and Technology, Fangzhen Lin Hong Kong University of Science and Technology DOI
11:18 18m Talk		Melocoton: A Program Logic for Verified Interoperability Between OCaml and C OOPSLA Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, Johannes Hostert ETH Zurich, Simon Spies MPI-SWS, Michael Sammler MPI-SWS, Lars Birkedal Aarhus University, Derek Dreyer MPI-SWS Link to publication DOI
11:36 18m Talk		Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning OOPSLA Noam Zilberstein Cornell University, Derek Dreyer MPI-SWS, Alexandra Silva Cornell University DOI Pre-print
11:54 18m Talk		Formal Abstractions for Packet Scheduling OOPSLA Anshuman Mohan Cornell University, Yunhe Liu Cornell University, Nate Foster Cornell University, Tobias Kappé Open University of the Netherlands; University of Amsterdam, Dexter Kozen Cornell University Link to publication DOI
12:12 18m Talk		P4R-Type: A Verified API for P4 Control Plane Programs OOPSLA Jens Kanstrup Larsen DTU, Roberto Guanciale KTH Royal Institute of Technology, Philipp Haller KTH Royal Institute of Technology, Alceste Scalas DTU DOI Pre-print Media Attached

11:00 - 12:30	distribution & networking 1OOPSLA at Room II Chair(s): Elisa Gonzalez Boix Vrije Universiteit Brussel

11:00 18m Talk		Initializing Global Objects: Time and Order OOPSLA Fengyun Liu Oracle Labs, Ondřej Lhoták University of Waterloo, David Hua University of Waterloo, Enze Xing University of Waterloo DOI
11:18 18m Talk		Type-Safe Dynamic Placement with First-Class Placed Values OOPSLA George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen DOI Pre-print
11:36 18m Talk		Secure RDTs: Enforcing Access Control Policies for Offline Available JSON Data OOPSLA Thierry Renaux Vrije Universiteit Brussel, Sam Van den Vonder Vrije Universiteit Brussel, Wolfgang De Meuter Vrije Universiteit Brussel DOI Pre-print
11:54 18m Talk		AtomiS: Data-Centric Synchronization Made Practical OOPSLA Hervé Paulino Nova University of Lisbon, Ana Almeida Matos University of Lisbon, Jan Cederquist University of Lisbon, Marco Giunti Nova University of Lisbon, João Batista Pereira Matos Júnior Sidia Instituto de Ciência e Tecnologia, António Ravara Nova University of Lisbon DOI
12:12 18m Talk		Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded Regions OOPSLA Christopher Wagner Purdue University, Nouraldin Jaber Purdue University, Roopsha Samanta Purdue University DOI

11:00 - 12:30	software developmentOOPSLA at Room XII Chair(s): Chandrakana Nandi Certora

11:00 18m Talk		Towards Better Semantics Exploration for Browser Fuzzing OOPSLA Chijin Zhou Tsinghua University, Quan Zhang Tsinghua University, Lihua Guo Tsinghua University, Mingzhe Wang Tsinghua University, Yu Jiang Tsinghua University, Qing Liao Harbin Institute of Technology, Zhiyong Wu National University of Defense Technology, Shanshan Li National University of Defense Technology, Bin Gu Beijing Institute of Control Engineering DOI
11:18 18m Talk		Live Pattern Matching with Typed Holes OOPSLA Yongwei Yuan Purdue University, Scott Guest University of Michigan, Eric Griffis University of Michigan, Hannah Potter University of Washington, David Moon University of Michigan, Cyrus Omar University of Michigan DOI
11:36 18m Talk		Interactive Debugging of Datalog Programs OOPSLA André Pacak JGU Mainz, Sebastian Erdweg JGU Mainz DOI
11:54 18m Talk		Accelerating Fuzzing through Prefix-Guided Execution OOPSLA Shaohua Li ETH Zurich, Zhendong Su ETH Zurich DOI
12:12 18m Talk		MemPerf: Profiling Allocator-Induced Performance Slowdowns OOPSLA Jin Zhou University of Massachusetts at Amherst, Sam Silvestro University of Texas at San Antonio, Steven (Jiaxun) Tang University of Massachusetts at Amherst, Hanmei Yang University of Massachusetts at Amherst, Hongyu Liu University of Texas at San Antonio, Guangming Zeng Synopsys, Bo Wu Colorado School of Mines, Cong Liu University of Texas at Dallas, Tongping Liu University of Massachusetts at Amherst DOI

	12:30 - 14:00	LunchCatering at Gallery

14:00 - 15:30	verification 2OOPSLA at Room I Chair(s): Jonathan Aldrich Carnegie Mellon University

14:00 18m Talk		Stuttering for Free OOPSLA Minki Cho Seoul National University, Youngju Song MPI-SWS, Dongjae Lee Seoul National University, Lennard Gäher MPI-SWS, Derek Dreyer MPI-SWS DOI
14:18 18m Talk		Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier OOPSLA Zhengyao Lin Carnegie Mellon University, Xiaohong Chen University of Illinois at Urbana-Champaign, Minh-Thai Trinh Advanced Digital Sciences Center, John Wang University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign DOI
14:36 18m Talk		Complete First-Order Reasoning for Properties of Functional Programs OOPSLA Adithya Murali University of Illinois at Urbana-Champaign, Lucas Peña University of Illinois at Urbana-Champaign, Ranjit Jhala University of California at San Diego, P. Madhusudan University of Illinois at Urbana-Champaign DOI
14:54 18m Talk		Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols OOPSLA Orr Tamir Tel Aviv University, Marcelo Taube Tel Aviv University, Kenneth L. McMillan University of Texas at Austin, Sharon Shoham Tel Aviv University, Jon Howell VMware Research, Guy Gueta VMware Research, Mooly Sagiv Tel Aviv University DOI
15:12 18m Talk		A conceptual framework for safe object initialization: a principled and mechanized soundness proof of the Celsius model OOPSLA Clément Blaudeau Inria, Fengyun Liu Oracle Labs Link to publication DOI

14:00 - 15:30	compilation and optimization 1OOPSLA at Room II Chair(s): Will Crichton Brown University

14:00 18m Talk		Formally Verifying Optimizations with Block Simulations OOPSLA Léo Gourdin Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, Benjamin Bonneau Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, Sylvain Boulmé Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, Alexandre Bérard Université Grenoble Alpes - CNRS - Grenoble INP - Verimag DOI Pre-print
14:18 18m Talk		Back to Direct Style: Typed and Tight OOPSLA Marius Müller University of Tübingen, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Klaus Ostermann University of Tübingen DOI Pre-print
14:36 18m Talk		Hardware-Aware Static Optimization of Hyperdimensional Computations OOPSLA Pu (Luke) Yi Stanford University, Sara Achour Stanford University DOI
14:54 18m Talk		Rapid: Region-Based Pointer Disambiguation OOPSLA Khushboo Chitre IIIT Delhi, Piyus Kedia IIIT Delhi, Rahul Purandare University of Nebraska-Lincoln DOI
15:12 18m Talk		Automated Ambiguity Detection in Layout-Sensitive Grammars OOPSLA Jiangyi Liu Tsinghua University, Fengmin Zhu CISPA - Helmholtz Center for Information Security, Fei He Tsinghua University DOI Pre-print

14:00 - 15:30	security & privacyOOPSLA at Room XII Chair(s): Arjun Guha Northeastern University; Roblox

14:00 18m Talk		Compositional Security Definitions for Higher-Order Where Declassification OOPSLA Jan Menz MPI-SWS, Andrew K. Hirsch University at Buffalo, SUNY, Peixuan Li Pennsylvania State University, Deepak Garg MPI-SWS DOI
14:18 18m Talk		Fat Pointers for Temporal Memory Safety of C OOPSLA Jie Zhou University of Rochester, John Criswell University of Rochester, Michael Hicks Amazon Web Services and the University of Maryland DOI
14:36 18m Talk		Quantifying and Mitigating Cache Side Channel Leakage with Differential Set OOPSLA Cong Ma University of Waterloo, Dinghao Wu Pennsylvania State University, Gang (Gary) Tan Pennsylvania State University, Mahmut Taylan Kandemir Pennsylvania State University, Danfeng Zhang Duke University; Pennsylvania State University DOI
14:54 18m Talk		A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations OOPSLA Anthony C. J. Fox ARM, Gareth Stockwell ARM, Shale Xiong ARM, Hanno Becker Amazon Web Services, Dominic P. Mulligan Amazon Web Services, Gustavo Petri Amazon Web Services, Nathan Chong Amazon Web Services DOI
15:12 18m Talk		Verifying Indistinguishability of Privacy-Preserving Protocols OOPSLA Kirby Linvill University of Colorado Boulder, Gowtham Kaki University of Colorado at Boulder, Eric Wustrow University of Colorado Boulder DOI

	15:30 - 16:00	Coffee BreakCatering at Gallery

16:00 - 17:30	distribution & networking 2OOPSLA at Room I Chair(s): Elisa Gonzalez Boix Vrije Universiteit Brussel

16:00 18m Talk		Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection OOPSLA Lorenzo Gheri University of Liverpool, Nobuko Yoshida University of Oxford DOI
16:18 18m Talk		Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity OOPSLA Chuta Sano McGill University, Ryan Kavanagh McGill University, Brigitte Pientka McGill University DOI
16:36 18m Talk		Message Chains for Distributed System Verification OOPSLA Federico Mora University of California at Berkeley, Ankush Desai Amazon Web Services, Elizabeth Polgreen University of Edinburgh, Sanjit A. Seshia University of California at Berkeley DOI
16:54 18m Talk		Randomized Testing of Byzantine Fault Tolerant Algorithms OOPSLA Levin N. Winter Delft University of Technology, Florena Buse Delft University of Technology, Daan de Graaf Delft University of Technology, Klaus von Gleissenthall Vrije Universiteit Amsterdam, Burcu Kulahcioglu Ozkan Delft University of Technology DOI
17:12 18m Talk		Validating IoT Devices with Rate-Based Session Types OOPSLA Grant Iraci University at Buffalo, Cheng-En Chuang University at Buffalo, Raymond Hu Queen Mary University of London, Lukasz Ziarek University at Buffalo DOI

16:00 - 17:30	refactoringOOPSLA at Room II Chair(s): Gowtham Kaki University of Colorado at Boulder

16:00 18m Talk		Aliasing Limits on Translating C to Safe Rust OOPSLA Mehmet Emre University of San Francisco, Peter Boyland University of California at Santa Barbara, Aesha Parekh University of California at Santa Barbara, Ryan Schroeder University of California at Santa Barbara, Kyle Dewey California State University, Ben Hardekopf University of California at Santa Barbara DOI Pre-print
16:18 18m Talk		Adventure of a Lifetime: Extract Method Refactoring for Rust OOPSLA Sewen Thy Ahrefs Research, Yale-NUS College, Andreea Costea National University of Singapore, Kiran Gopinathan National University of Singapore, Ilya Sergey National University of Singapore DOI Pre-print
16:36 18m Talk		Inductive Program Synthesis Guided by Observational Program Similarity OOPSLA Jack Feser Hamilton College, Işıl Dillig University of Texas at Austin, Armando Solar-Lezama Massachusetts Institute of Technology DOI
16:54 18m Talk		Automated Translation of Functional Big Data Queries to SQL OOPSLA Guoqiang Zhang North Carolina State University, Benjamin Mariano University of Texas at Austin, Xipeng Shen North Carolina State University, Işıl Dillig University of Texas at Austin DOI
17:12 18m Talk		User-Customizable Transpilation of Scripting Languages OOPSLA Bo Wang National University of Singapore, Aashish Kolluri National University of Singapore, Ivica Nikolić National University of Singapore, Teodora Baluta National University of Singapore, Prateek Saxena National University of Singapore DOI

16:00 - 17:30	separation logicOOPSLA at Room XII Chair(s): Jonathan Aldrich Carnegie Mellon University

16:00 18m Talk		Verification-Preserving Inlining in Automatic Separation Logic Verifiers OOPSLA Thibault Dardinier ETH Zurich, Gaurav Parthasarathy ETH Zurich, Peter Müller ETH Zurich DOI
16:18 18m Talk		Leaf: Modularity for Temporary Sharing in Separation Logic OOPSLA Travis Hance Carnegie Mellon University, Jon Howell VMware Research, Oded Padon VMware Research, Bryan Parno Carnegie Mellon University DOI
16:36 18m Talk		Proof Automation for Linearizability in Separation Logic OOPSLA Ike Mulder Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen DOI Pre-print
16:54 18m Talk		Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic OOPSLA Jaehwang Jung KAIST, Janggun Lee KAIST, Jaemin Choi KAIST, Jaewoo Kim KAIST, Sunho Park KAIST, Jeehoon Kang KAIST DOI
17:12 18m Talk		Functional collection programming with semi-ring dictionaries OOPSLA Amir Shaikhha University of Edinburgh, Mathieu Huot University of Oxford, Jaclyn Smith Oxford University, Dan Olteanu University of Zurich Link to publication DOI

Not scheduled yet

	Not scheduled yet Talk		Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory OOPSLA Simon Friis Vindum Aarhus University, Lars Birkedal Aarhus University DOI
	Not scheduled yet Talk		Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks OOPSLA Pengfei Gao ShanghaiTech University, Yedi Zhang ShanghaiTech University, Fu Song State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, and University of Chinese Academy of Sciences Beijing, China, Taolue Chen University of London, Francois-Xavier Standaert Université Catholique de Louvain DOI
	Not scheduled yet Talk		Two Birds with One Stone: Boosting Code Generation and Code Search via a Generative Adversarial Network OOPSLA Shangwen Wang National University of Defense Technology, Bo Lin National University of Defense Technology, Zhensu Sun Singapore Management University, Ming Wen Huazhong University of Science and Technology, Yepang Liu Southern University of Science and Technology, Yan Lei Chongqing University, Xiaoguang Mao National University of Defense Technology DOI Pre-print

Accepted Papers

	Title
	Accelerating Fuzzing through Prefix-Guided Execution OOPSLA Shaohua Li, Zhendong Su DOI
	A Cocktail Approach to Practical Call Graph Construction OOPSLA Yuandao Cai, Charles Zhang DOI
	A Container-Usage-Pattern-Based Context Debloating Approach for Object-Sensitive Pointer Analysis OOPSLA Dongjie He, Yujiang Gui, Wei Li, Yonggang Tao, Changwei Zou, Yulei Sui, Jingling Xue DOI Pre-print
	A Deductive Verification Infrastructure for Probabilistic Programs OOPSLA Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja DOI
	Adventure of a Lifetime: Extract Method Refactoring for Rust OOPSLA Sewen Thy, Andreea Costea, Kiran Gopinathan, Ilya Sergey DOI Pre-print
	A Gradual Probabilistic Lambda Calculus OOPSLA Wenjia Ye, Matías Toro, Federico Olmedo DOI
	A Grounded Conceptual Model for Ownership Types in Rust OOPSLA Will Crichton, Gavin Gray, Shriram Krishnamurthi DOI Pre-print
	Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs OOPSLA Amir Kafshdar Goharshady, S. Hitarth, Fatemeh Mohammadi, Harshit Jitendra Motwani DOI
	Aliasing Limits on Translating C to Safe Rust OOPSLA Mehmet Emre, Peter Boyland, Aesha Parekh, Ryan Schroeder, Kyle Dewey, Ben Hardekopf DOI Pre-print
	An Explanation Method for Models of Code OOPSLA Yu Wang, Ke Wang, Linzhang Wang DOI
	A Pretty Expressive Printer OOPSLA Sorawee Porncharoenwase, Justin Pombrio, Emina Torlak DOI Pre-print
	Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart Contracts OOPSLA Zhuo Cai, Soroush Farokhnia, Amir Kafshdar Goharshady, S. Hitarth DOI
	AST vs. Bytecode: Interpreters in the Age of Meta-Compilation OOPSLA Octave Larose, Sophie Kaleba, Humphrey Burchell, Stefan Marr DOI Pre-print
	AtomiS: Data-Centric Synchronization Made Practical OOPSLA Hervé Paulino, Ana Almeida Matos, Jan Cederquist, Marco Giunti, João Batista Pereira Matos Júnior, António Ravara DOI
	Automated Ambiguity Detection in Layout-Sensitive Grammars OOPSLA Jiangyi Liu, Fengmin Zhu, Fei He DOI Pre-print
	Automated Translation of Functional Big Data Queries to SQL OOPSLA Guoqiang Zhang, Benjamin Mariano, Xipeng Shen, Işıl Dillig DOI
	A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations OOPSLA Anthony C. J. Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Dominic P. Mulligan, Gustavo Petri, Nathan Chong DOI
	Back to Direct Style: Typed and Tight OOPSLA Marius Müller, Philipp Schuster, Jonathan Immanuel Brachthäuser, Klaus Ostermann DOI Pre-print
	Beacons: An End-to-End Compiler Framework for Predicting and Utilizing Dynamic Loop Characteristics OOPSLA Girish Mururu, Sharjeel Khan, Bodhisatwa Chatterjee, Chao Chen, Chris Porter, Ada Gavrilovska, Santosh Pande DOI
	Bidirectional Object-Oriented Programming: Towards Programmatic and Direct Manipulation of Objects OOPSLA Xing Zhang, Guanchen Guo, Xiao He, Zhenjiang Hu DOI
	Bring Your Own Data Structures to Datalog OOPSLA Arash Sahebolamri, Langston Barrett, Scott Moore, Kristopher Micinski DOI
	Building Dynamic System Call Sandbox with Partial Order Analysis OOPSLA Quan Zhang, Chijin Zhou, Yiwen Xu, Zijing Yin, Mingzhe Wang, Zhuo Su, Chengnian Sun, Yu Jiang, Jiaguang Sun DOI
	Compiling Structured Tensor Algebra OOPSLA Mahdi Ghorbani, Mathieu Huot, Shideh Hashemian, Amir Shaikhha DOI
	Complete First-Order Reasoning for Properties of Functional Programs OOPSLA Adithya Murali, Lucas Peña, Ranjit Jhala, P. Madhusudan DOI
	Compositional Security Definitions for Higher-Order Where Declassification OOPSLA Jan Menz, Andrew K. Hirsch, Peixuan Li, Deepak Garg DOI
	Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks OOPSLA Pengfei Gao, Yedi Zhang, Fu Song, Taolue Chen, Francois-Xavier Standaert DOI
	Concrete Type Inference for Code Optimization using Machine Learning with SMT Solving OOPSLA Fangke Ye, Jisheng Zhao, Jun Shirako, Vivek Sarkar DOI
	Continuing WebAssembly with Effect Handlers OOPSLA Luna Phipps-Costin, Andreas Rossberg, Arjun Guha, Daan Leijen, Daniel Hillerström, KC Sivaramakrishnan, Matija Pretnar, Sam Lindley DOI Pre-print
	Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols OOPSLA Orr Tamir, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta, Mooly Sagiv DOI
	Data Extraction via Semantic Regular Expression Synthesis OOPSLA Jocelyn (Qiaochu) Chen, Arko Banerjee, Çağatay Demiralp, Greg Durrett, Işıl Dillig DOI
	Deep Learning Robustness Verification for Few-Pixel Attacks OOPSLA Yuval Shapira, Eran Avneri, Dana Drachsler Cohen DOI
	Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded Regions OOPSLA Christopher Wagner, Nouraldin Jaber, Roopsha Samanta DOI
	Equality Saturation Theory Exploration à la Carte OOPSLA Anjali Pal, Brett Saiki, Ryan Tjoa, Cynthia Richey, Amy Zhu, Oliver Flatt, Max Willsey, Zachary Tatlock, Chandrakana Nandi DOI Pre-print
	Exact Recursive Probabilistic Programming OOPSLA David Chiang, Colin McDonald, Chung-chieh Shan DOI
	Explainable Program Synthesis by Localizing Specifications OOPSLA Amirmohammad Nazari, Yifei Huang, Roopsha Samanta, Arjun Radhakrishna, Mukund Raghothaman DOI
	Exploiting the Sparseness of Control-Flow and Call Graphs for Efficient and On-Demand Algebraic Program Analysis OOPSLA Giovanna Kobus Conrado, Amir Kafshdar Goharshady, Kerim Kochekov, Yun Chen Tsai, Ahmed Khaled Zaher DOI
	Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems OOPSLA Magnus Madsen, Jaco van de Pol, Troels Henriksen DOI
	Fat Pointers for Temporal Memory Safety of C OOPSLA Jie Zhou, John Criswell, Michael Hicks DOI
	Fluent APIs in Functional Languages OOPSLA Ori Roth, Yossi Gil DOI Pre-print
	Formal Abstractions for Packet Scheduling OOPSLA Anshuman Mohan, Yunhe Liu, Nate Foster, Tobias Kappé, Dexter Kozen Link to publication DOI
	Formally Verifying Optimizations with Block Simulations OOPSLA Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard DOI Pre-print
	From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers OOPSLA Marius Müller, Philipp Schuster, Jonathan Lindegaard Starup, Klaus Ostermann, Jonathan Immanuel Brachthäuser Link to publication DOI Pre-print
	Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier OOPSLA Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Roşu DOI
	Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference OOPSLA Ishan Bhanuka, Lionel Parreaux, David Binder, Jonathan Immanuel Brachthäuser DOI Pre-print
	Gradual Typing for Effect Handlers OOPSLA Max S. New, Eric Giovannini, Daniel R. Licata DOI
	Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies OOPSLA Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, Tiark Rompf DOI Pre-print
	Greedy Implicit Bounded Quantification OOPSLA Chen Cui, Shengyi Jiang, Bruno C. d. S. Oliveira DOI
	Grounded Copilot: How Programmers Interact with Code-Generating Models OOPSLA Shraddha Barke, Michael B. James, Nadia Polikarpova DOI
	Hardware-Aware Static Optimization of Hyperdimensional Computations OOPSLA Pu (Luke) Yi, Sara Achour DOI
	Historia: Refuting Callback Reachability with Message-History Logics OOPSLA Shawn Meier, Sergio Mover, Gowtham Kaki, Bor-Yuh Evan Chang DOI
	How Domain Experts Use an Embedded DSL OOPSLA Lisa Rennels, Sarah E. Chasins DOI
	How Profilers Can Help Navigate Type Migration OOPSLA Ben Greenman, Matthias Felleisen, Christos Dimoulas DOI
	Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection OOPSLA Lorenzo Gheri, Nobuko Yoshida DOI
	Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection OOPSLA Ruyi Ji, Chaozhe Kong, Yingfei Xiong, Zhenjiang Hu DOI
	Inductive Program Synthesis Guided by Observational Program Similarity OOPSLA Jack Feser, Işıl Dillig, Armando Solar-Lezama DOI
	Inference of Resource Management Specifications OOPSLA Narges Shadab, Pritam Gharat, Shrey Tiwari, Michael D. Ernst, Martin Kellogg, Shuvendu K. Lahiri, Akash Lal, Manu Sridharan DOI
	Initializing Global Objects: Time and Order OOPSLA Fengyun Liu, Ondřej Lhoták, David Hua, Enze Xing DOI
	Interactive Debugging of Datalog Programs OOPSLA André Pacak, Sebastian Erdweg DOI
	Languages with Decidable Learning: A Meta-theorem OOPSLA Paul Krogmeier, P. Madhusudan DOI
	Leaf: Modularity for Temporary Sharing in Separation Logic OOPSLA Travis Hance, Jon Howell, Oded Padon, Bryan Parno DOI
	Live Pattern Matching with Typed Holes OOPSLA Yongwei Yuan, Scott Guest, Eric Griffis, Hannah Potter, David Moon, Cyrus Omar DOI
	Lower Bounds for Possibly Divergent Probabilistic Programs OOPSLA Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan Link to publication DOI Pre-print
	Mat2Stencil: A Modular Matrix-Based DSL for Explicit and Implicit Matrix-Free PDE Solvers on Structured Grid OOPSLA Huanqi Cao, Shizhi Tang, Qianchao Zhu, Bowen Yu, Wenguang Chen DOI
	Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity OOPSLA Chuta Sano, Ryan Kavanagh, Brigitte Pientka DOI
	Melocoton: A Program Logic for Verified Interoperability Between OCaml and C OOPSLA Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer Link to publication DOI
	MemPerf: Profiling Allocator-Induced Performance Slowdowns OOPSLA Jin Zhou, Sam Silvestro, Steven (Jiaxun) Tang, Hanmei Yang, Hongyu Liu, Guangming Zeng, Bo Wu, Cong Liu, Tongping Liu DOI
	Message Chains for Distributed System Verification OOPSLA Federico Mora, Ankush Desai, Elizabeth Polgreen, Sanjit A. Seshia DOI
	Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates OOPSLA Aalok Thakkar, Nathaniel Sands, Georgios Petrou, Rajeev Alur, Mayur Naik, Mukund Raghothaman DOI
	Modular Component-Based Quantum Circuit Synthesis OOPSLA Chan Gu Kang, Hakjoo Oh DOI
	Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic OOPSLA Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, Jeehoon Kang DOI
	Mutually Iso-Recursive Subtyping OOPSLA Andreas Rossberg DOI
	Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning OOPSLA Noam Zilberstein, Derek Dreyer, Alexandra Silva DOI Pre-print
	P4R-Type: A Verified API for P4 Control Plane Programs OOPSLA Jens Kanstrup Larsen, Roberto Guanciale, Philipp Haller, Alceste Scalas DOI Pre-print Media Attached
	Perception Contracts for Safety of ML-Enabled Systems OOPSLA Angello Astorga, Chiao Hsieh, P. Madhusudan, Sayan Mitra DOI
	Proof Automation for Linearizability in Separation Logic OOPSLA Ike Mulder, Robbert Krebbers DOI Pre-print
	Pushing the Limit of 1-Minimality of Language-Agnostic Program Reduction OOPSLA Zhenyang Xu, Yongqiang Tian, Mengxiao Zhang, Gaosen Zhao, Yu Jiang, Chengnian Sun DOI
	Quantifying and Mitigating Cache Side Channel Leakage with Differential Set OOPSLA Cong Ma, Dinghao Wu, Gang (Gary) Tan, Mahmut Taylan Kandemir, Danfeng Zhang DOI
	Randomized Testing of Byzantine Fault Tolerant Algorithms OOPSLA Levin N. Winter, Florena Buse, Daan de Graaf, Klaus von Gleissenthall, Burcu Kulahcioglu Ozkan DOI
	Rapid: Region-Based Pointer Disambiguation OOPSLA Khushboo Chitre, Piyus Kedia, Rahul Purandare DOI
	Reference Capabilities for Flexible Memory Management OOPSLA Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew J. Parkinson, Tobias Wrigstad DOI Pre-print
	Regular Expression Matching using Bit Vector Automata OOPSLA Alexis Le Glaunec, Lingkun Kong, Konstantinos Mamouras DOI
	Resource-Aware Soundness for Big-Step Semantics OOPSLA Riccardo Bianchini, Francesco Dagnino, Paola Giannini, Elena Zucca DOI
	Reusing Just-in-Time Compiled Code OOPSLA Meetesh Kalpesh Mehta, Sebastián Krynski, Hugo Musso Gualandi, Manas Thakur, Jan Vitek DOI
	Rhombus: A New Spin on Macros without All the Parentheses OOPSLA Matthew Flatt, Taylor Allred, Nia Angle, Stephen De Gabrielle, Robert Bruce Findler, Jack Firth, Kiran Gopinathan, Ben Greenman, Siddhartha Kasivajhula, Alex Knauth, Jay McCarthy, Sam Phillips, Sorawee Porncharoenwase, Jens Axel Søgaard, Sam Tobin-Hochstadt DOI Pre-print
	Run-Time Prevention of Software Integration Failures of Machine Learning APIs OOPSLA Chengcheng Wan, Yuhan Liu, Kuntai Du, Henry Hoffmann, Junchen Jiang, Michael Maire, Shan Lu DOI
	Saggitarius: A DSL for Specifying Grammatical Domains OOPSLA Anders Miltner, Devon Loehr, Arnold Mong, Kathleen Fisher, David Walker DOI
	Secure RDTs: Enforcing Access Control Policies for Offline Available JSON Data OOPSLA Thierry Renaux, Sam Van den Vonder, Wolfgang De Meuter DOI Pre-print
	Simple Reference Immutability for System F<: OOPSLA Edward Lee, Ondřej Lhoták DOI
	Solving Conditional Linear Recurrences for Program Verification: The Periodic Case OOPSLA Chenglin Wang, Fangzhen Lin DOI
	Solving String Constraints with Lengths by Stabilization OOPSLA Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Juraj Síč DOI
	Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory OOPSLA Simon Friis Vindum, Lars Birkedal DOI
	Static Analysis of Memory Models for SMT Encodings OOPSLA Thomas Haas, René Maseli, Roland Meyer, Hernán Ponce de León DOI
	Structural Subtyping as Parametric Polymorphism OOPSLA Wenhao Tang, Daniel Hillerström, James McKinna, Michel Steuwer, Ornela Dardha, Rongxiao Fu, Sam Lindley DOI Pre-print
	Stuttering for Free OOPSLA Minki Cho, Youngju Song, Dongjae Lee, Lennard Gäher, Derek Dreyer DOI
	Synthesizing Efficient Memoization Algorithms OOPSLA Yican Sun, Xuanyu Peng, Yingfei Xiong DOI
	Synthesizing Precise Static Analyzers for Automatic Differentiation OOPSLA Jacob Laurel, Siyuan Brant Qian, Gagandeep Singh, Sasa Misailovic DOI
	Synthesizing Specifications OOPSLA Kanghee Park, Loris D'Antoni, Thomas Reps DOI
	TASTyTruffle: Just-in-Time Specialization of Parametric Polymorphism OOPSLA Matt D'Souza, James You, Ondřej Lhoták, Aleksandar Prokopec DOI
	The Bounded Pathwidth of Control-Flow Graphs OOPSLA Giovanna Kobus Conrado, Amir Kafshdar Goharshady, Chun Kit Lam DOI
	The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog OOPSLA Qinlin Chen, Nairen Zhang, Jinpeng Wang, Tian Tan, Chang Xu, Xiaoxing Ma, Yue Li DOI
	Towards Better Semantics Exploration for Browser Fuzzing OOPSLA Chijin Zhou, Quan Zhang, Lihua Guo, Mingzhe Wang, Yu Jiang, Qing Liao, Zhiyong Wu, Shanshan Li, Bin Gu DOI
	Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs OOPSLA Alex Renda, Yi Ding, Michael Carbin DOI Pre-print
	Two Birds with One Stone: Boosting Code Generation and Code Search via a Generative Adversarial Network OOPSLA Shangwen Wang, Bo Lin, Zhensu Sun, Ming Wen, Yepang Liu, Yan Lei, Xiaoguang Mao DOI Pre-print
	Type-Safe Dynamic Placement with First-Class Placed Values OOPSLA George Zakhour, Pascal Weisenburger, Guido Salvaneschi DOI Pre-print
	User-Customizable Transpilation of Scripting Languages OOPSLA Bo Wang, Aashish Kolluri, Ivica Nikolić, Teodora Baluta, Prateek Saxena DOI
	Validating IoT Devices with Rate-Based Session Types OOPSLA Grant Iraci, Cheng-En Chuang, Raymond Hu, Lukasz Ziarek DOI
	Verification-Preserving Inlining in Automatic Separation Logic Verifiers OOPSLA Thibault Dardinier, Gaurav Parthasarathy, Peter Müller DOI
	Verifying Indistinguishability of Privacy-Preserving Protocols OOPSLA Kirby Linvill, Gowtham Kaki, Eric Wustrow DOI
	Verus: Verifying Rust Programs using Linear Ghost Types OOPSLA Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel DOI
	When Concurrency Matters: Behaviour-Oriented Concurrency OOPSLA Luke Cheeseman, Matthew J. Parkinson, Sylvan Clebsch, Marios Kogias, Sophia Drossopoulou, David Chisnall, Tobias Wrigstad, Paul Liétar DOI

Call for Papers

The OOPSLA issue of the Proceedings of the ACM on Programming Languages (PACMPL) welcomes papers focusing on all practical and theoretical investigations of programming languages, systems and environments. Papers may target any stage of software development, including requirements, modeling, prototyping, design, implementation, generation, analysis, verification, testing, evaluation, maintenance, and reuse of software systems. Contributions may include the development of new tools, techniques, principles, and evaluations.

OOPSLA 2023 will have two separate rounds of reviewing, with Round 1 submission deadline: October 28, 2022 and and Round 2 submission deadline: April 14, 2023
In each round, papers will have a final outcome of Accept, Revise, or Reject—see Review Process for details.

Papers accepted at either of the rounds will be published in the 2023 volume of PACMPL(OOPSLA) and invited to be presented at the SPLASH conference in October 2023.

Review Process

PACMPL(OOPSLA) has two rounds of reviewing. The final outcome of each round can be one of Accept, Revise or Reject.

Accept: Accepted papers will appear in the 2023 volume of PACMPL(OOPSLA).

Revise: Papers in this category are invited to submit a revision to the next round of submissions with a specific set of expectations to be met. When authors resubmit, they should clearly explain how the revisions address the comments of the reviewers, by including a document describing the changes and – if possible – a diff of the PDF as supplementary material. The revised paper will be re-evaluated, and either accepted or rejected. Resubmitted papers will retain the same reviewers throughout the process. Papers with a Revise outcome in Round 2 and an Accept outcome in the subsequent Round 1 will appear in the 2024 volume of PACMPL(OOPSLA).

Reject: Rejected papers will not be included in the 2023 volume of PACMPL(OOPSLA). Papers in this category are not guaranteed a review if resubmitted less than one year from the date of original submission. A paper will be judged to be a resubmission if it is substantially similar to the original submission. The judgment that a paper is a resubmission of the same work and whether, in this case, it will be reviewed or not is at the discretion of the Chair. Obviously, this same policy applies to papers that were rejected for inclusion in the 2022 volume of PACMPL(OOPSLA).

Each round of reviewing consists of two phases. The first phase evaluates the papers and results in an early notification of Reject, Revise, or Conditional Accept. During the first phase, authors will be able to read their reviews and respond to them. The second phase is restricted to conditionally accepted papers. Authors must make a set of mandatory revisions. The second phase assesses whether the required revisions have been addressed. The outcome can be Accept, Revise or Reject.

Submissions

Submitted papers (including resubmissions) must be at most 23 pages using the template below. The references do not count towards this limit. No appendices are allowed on the main paper, instead authors can upload supplementary material with no page or content restrictions, but reviewers may choose to ignore it. The PACMPL templates used for SPLASH (Microsoft Word and LaTeX) can be found at the SIGPLAN author information page. In particular, authors using LaTeX should use the acmart-pacmpl-template.tex file (with the acmsmall option). Papers are expected to use author-year citations. Author-year citations may be used as either a noun phrase, such as “The lambda calculus was originally conceived by Church (1932)”, or a parenthetic phase, such as “The lambda calculus (Church 1932) was intended as a foundation for mathematics”.

PACMPL uses double-blind reviewing. Authors’ identities are only revealed if a paper is accepted. Papers must

omit author names and institutions,
use the third person when referencing your work,
anonymise supplementary material.

Nothing should be done in the name of anonymity that weakens the submission; see the DBR FAQ. When in doubt, contact the Review Committee Chairs.

Papers must describe unpublished work that is not currently submitted for publication elsewhere as described by SIGPLAN’s Republication Policy. Submitters should also be aware of ACM’s Policy and Procedures on Plagiarism. Submissions are expected to comply with the ACM Policies for Authorship.

Artifacts

Authors should indicate with their initial submission if an artifact exists, describe its nature and limitations, and indicate if it will be submitted for evaluation. Accepted papers that fail to provide an artifact will be requested to explain the reason they cannot support replication. It is understood that some papers have no artifacts.

Publication

PACMPL is a Gold Open Access journal, all papers will be freely available to the public. Authors can voluntarily cover the article processing charge ($400), but payment is not required. The official publication date is the date the journal are made available in the ACM Digital Library. The journal issue and associated papers may be published up to two weeks prior to the first day of the conference. The official publication date affects the deadline for any patent filings related to published work.

FAQ

Selection Criteria

We consider the following criteria when evaluating papers:

Novelty: The paper presents new ideas and results and places them appropriately within the context established by previous research.

Importance: The paper contributes to the advancement of knowledge in the field. We also welcome papers that diverge from the dominant trajectory of the field.

Evidence: The paper presents sufficient evidence supporting its claims, such as proofs, implemented systems, experimental results, statistical analyses, case studies, and anecdotes.

Clarity: The paper presents its contributions, methodology and results clearly.

Artifacts

Q: Are artifacts required?

No! It is understood that some papers have no artifacts. But if an artifact is not provided when the claims in the paper refer to an artifact, the authors must explain why their work is not available for repetition.

Q: Can a paper be accepted if the artifact is rejected?

Yes! The reasons for rejecting an artifact are multiple and often stem from the quality of the packaging.

Double-Blinding Submissions (Authors)

Q: What exactly do I have to do to anonymize my paper?

Use common sense. Your job is not to make your identity undiscoverable but simply to make it possible for reviewers to evaluate your submission without having to know who you are. The specific guidelines stated in the call for papers are simple: omit authors’ names from your title page, and when you cite your own work, refer to it in the third person. For example, if your name is Smith and you have worked on amphibious type systems, instead of saying “We extend our earlier work on statically typed toads [Smith 2004],” you might say “We extend Smith’s [2004] earlier work on statically typed toads.” Also, be sure not to include any acknowledgements that would give away your identity.

Q: Should I change the name of my system?

No.

Q: My submission is based on code available in a public repository. How do I deal with this?

Cite the code in your paper, but remove the URL and, instead say “link to repository removed for double blind review”. If you believe reviewer access to your code would help during author response, contact the Review Committee Chairs.

Q: I am submitting an extension of my workshop paper, should I anonymize reference to that work?

No. But we recommend you do not use the same title, so that it is clearly distinguishes the papers.

Q: Am I allowed to post my paper on my web page or arXiv? send it to colleagues? give a talk about it? on social media?

We have developed guidelines to help navigate the tension between the normal communication of scientific results and actions that essentially force potential reviewers to learn the identity of authors. Roughly speaking, you may discuss work under submission, but you should not broadly advertise your work through media that is likely to reach your reviewers. We acknowledge there are gray areas and trade-offs. Things you may do:

Put your submission on your home page.
Discuss your work with anyone not on the review committees or reviewers with whom you already have a conflict.
Present your work at professional meetings, job interviews, etc.
Submit work previously discussed at an informal workshop, previously posted on arXiv or a similar site, previously submitted to a conference not using double-blind reviewing, etc.

Things you should not do:

Contact members of the review committee about your work, or deliberately present your work where you expect them to be.
Publicize your work on social media if wide public [re-]propagation is common (e.g., Twitter) and therefore likely to reach potential reviewers. For example, on Facebook, a post with a broad privacy setting (public or all friends) saying, “Whew, OOPSLA paper in, time to sleep” is okay, but one describing the work or giving its title is not appropriate. Alternately, a post to a group including only the colleagues at your institution is fine.

Reviewers will not be asked to recuse themselves from reviewing your paper unless they feel you have gone out of your way to advertise your authorship information to them. If you are unsure about what constitutes “going out of your way”, please contact the Review Committee Chairs.

Cascais

Lisboa

Palácio da Pena

Quinta da Regaleira

Pastel de Belém

Terreiro do Paço

Castelo de São Jorge

Linha de Cascais

Coastal Train Line between Lisbon and Cascais

OOPSLASPLASH 2023

Program Display Configuration

Wed 25 OctDisplayed time zone: Lisbon change

Thu 26 OctDisplayed time zone: Lisbon change

Fri 27 OctDisplayed time zone: Lisbon change

Not scheduled yet

Accepted Papers

Call for Papers

Mira MeziniPC Chair

TU Darmstadt

Germany

Derek DreyerAssociate Chair

MPI-SWS

Germany

Sophia DrossopoulouAssociate Chair

Imperial College London

United Kingdom

Patrick EugsterAssociate Chair

USI Lugano; Purdue University

Switzerland

Shriram KrishnamurthiAssociate Chair

Brown University

United States

Jonathan Aldrich

Carnegie Mellon University

United States

Karim Ali

University of Alberta

Peter Alvaro

University of California, Santa Cruz

Stephanie Balzer

Carnegie Mellon University

United States

Osbert Bastani

University of Pennsylvania

United States

Annette Bieniusa

University of Kaiserslautern-Landau

Germany

Sebastian Burckhardt

Microsoft Research

United States

Satish Chandra

Meta Platforms

United States

James Cheney

University of Edinburgh

United Kingdom

Pavel Chuprikov

USI Lugano

Switzerland

Albert Cohen

Google

France

Wolfgang De Meuter

Vrije Universiteit Brussel

Belgium

Dominique Devriese

KU Leuven

Belgium

Dana Drachsler Cohen

Technion

Israel

Jana Dunfield

Queen's University, Kingston, Ontario

Canada

Sebastian Erdweg

JGU Mainz

Germany

Matthew Flatt

University of Utah

Wed 25 Oct
Displayed time zone: Lisbon change

Thu 26 Oct
Displayed time zone: Lisbon change

Fri 27 Oct
Displayed time zone: Lisbon change