SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Dates
Plenary
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

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 ModelsDistinguished Paper
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
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-theoremDistinguished Paper
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 ProgramsDistinguished Paper
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 StabilizationDistinguished Paper
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
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 DatalogDistinguished Paper
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
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
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 SchedulingDistinguished Paper
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 OrderDistinguished Paper
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 HolesDistinguished Paper
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 ExecutionDistinguished Paper
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
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 AlgorithmsDistinguished Paper
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 MemoryDistinguished Paper
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 ExecutionDistinguished Paper
OOPSLA
DOI
A Cocktail Approach to Practical Call Graph Construction
OOPSLA
DOI
A Container-Usage-Pattern-Based Context Debloating Approach for Object-Sensitive Pointer Analysis
OOPSLA
DOI Pre-print
A Deductive Verification Infrastructure for Probabilistic Programs
OOPSLA
DOI
Adventure of a Lifetime: Extract Method Refactoring for Rust
OOPSLA
DOI Pre-print
A Gradual Probabilistic Lambda Calculus
OOPSLA
DOI
A Grounded Conceptual Model for Ownership Types in Rust
OOPSLA
DOI Pre-print
Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial ProgramsDistinguished Paper
OOPSLA
DOI
Aliasing Limits on Translating C to Safe Rust
OOPSLA
DOI Pre-print
An Explanation Method for Models of Code
OOPSLA
DOI
A Pretty Expressive Printer
OOPSLA
DOI Pre-print
Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart Contracts
OOPSLA
DOI
AST vs. Bytecode: Interpreters in the Age of Meta-Compilation
OOPSLA
DOI Pre-print
AtomiS: Data-Centric Synchronization Made Practical
OOPSLA
DOI
Automated Ambiguity Detection in Layout-Sensitive Grammars
OOPSLA
DOI Pre-print
Automated Translation of Functional Big Data Queries to SQL
OOPSLA
DOI
A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations
OOPSLA
DOI
Back to Direct Style: Typed and Tight
OOPSLA
DOI Pre-print
Beacons: An End-to-End Compiler Framework for Predicting and Utilizing Dynamic Loop Characteristics
OOPSLA
DOI
Bidirectional Object-Oriented Programming: Towards Programmatic and Direct Manipulation of Objects
OOPSLA
DOI
Bring Your Own Data Structures to DatalogDistinguished Paper
OOPSLA
DOI
Building Dynamic System Call Sandbox with Partial Order Analysis
OOPSLA
DOI
Compiling Structured Tensor Algebra
OOPSLA
DOI
Complete First-Order Reasoning for Properties of Functional Programs
OOPSLA
DOI
Compositional Security Definitions for Higher-Order Where Declassification
OOPSLA
DOI
Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks
OOPSLA
DOI
Concrete Type Inference for Code Optimization using Machine Learning with SMT Solving
OOPSLA
DOI
Continuing WebAssembly with Effect Handlers
OOPSLA
DOI Pre-print
Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols
OOPSLA
DOI
Data Extraction via Semantic Regular Expression Synthesis
OOPSLA
DOI
Deep Learning Robustness Verification for Few-Pixel Attacks
OOPSLA
DOI
Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded Regions
OOPSLA
DOI
Equality Saturation Theory Exploration à la Carte
OOPSLA
DOI Pre-print
Exact Recursive Probabilistic Programming
OOPSLA
DOI
Explainable Program Synthesis by Localizing Specifications
OOPSLA
DOI
Exploiting the Sparseness of Control-Flow and Call Graphs for Efficient and On-Demand Algebraic Program Analysis
OOPSLA
DOI
Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems
OOPSLA
DOI
Fat Pointers for Temporal Memory Safety of C
OOPSLA
DOI
Fluent APIs in Functional Languages
OOPSLA
DOI Pre-print
Formal Abstractions for Packet SchedulingDistinguished Paper
OOPSLA
Link to publication DOI
Formally Verifying Optimizations with Block Simulations
OOPSLA
DOI Pre-print
From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers
OOPSLA
Link to publication DOI Pre-print
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier
OOPSLA
DOI
Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference
OOPSLA
DOI Pre-print
Gradual Typing for Effect Handlers
OOPSLA
DOI
Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies
OOPSLA
DOI Pre-print
Greedy Implicit Bounded Quantification
OOPSLA
DOI
Grounded Copilot: How Programmers Interact with Code-Generating ModelsDistinguished Paper
OOPSLA
DOI
Hardware-Aware Static Optimization of Hyperdimensional Computations
OOPSLA
DOI
Historia: Refuting Callback Reachability with Message-History Logics
OOPSLA
DOI
How Domain Experts Use an Embedded DSL
OOPSLA
DOI
How Profilers Can Help Navigate Type Migration
OOPSLA
DOI
Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection
OOPSLA
DOI
Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection
OOPSLA
DOI
Inductive Program Synthesis Guided by Observational Program Similarity
OOPSLA
DOI
Inference of Resource Management Specifications
OOPSLA
DOI
Initializing Global Objects: Time and OrderDistinguished Paper
OOPSLA
DOI
Interactive Debugging of Datalog Programs
OOPSLA
DOI
Languages with Decidable Learning: A Meta-theoremDistinguished Paper
OOPSLA
DOI
Leaf: Modularity for Temporary Sharing in Separation Logic
OOPSLA
DOI
Live Pattern Matching with Typed HolesDistinguished Paper
OOPSLA
DOI
Lower Bounds for Possibly Divergent Probabilistic Programs
OOPSLA
Link to publication DOI Pre-print
Mat2Stencil: A Modular Matrix-Based DSL for Explicit and Implicit Matrix-Free PDE Solvers on Structured Grid
OOPSLA
DOI
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity
OOPSLA
DOI
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
OOPSLA
Link to publication DOI
MemPerf: Profiling Allocator-Induced Performance Slowdowns
OOPSLA
DOI
Message Chains for Distributed System Verification
OOPSLA
DOI
Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates
OOPSLA
DOI
Modular Component-Based Quantum Circuit Synthesis
OOPSLA
DOI
Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic
OOPSLA
DOI
Mutually Iso-Recursive Subtyping
OOPSLA
DOI
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
OOPSLA
DOI Pre-print
P4R-Type: A Verified API for P4 Control Plane Programs
OOPSLA
DOI Pre-print Media Attached
Perception Contracts for Safety of ML-Enabled Systems
OOPSLA
DOI
Proof Automation for Linearizability in Separation Logic
OOPSLA
DOI Pre-print
Pushing the Limit of 1-Minimality of Language-Agnostic Program Reduction
OOPSLA
DOI
Quantifying and Mitigating Cache Side Channel Leakage with Differential Set
OOPSLA
DOI
Randomized Testing of Byzantine Fault Tolerant AlgorithmsDistinguished Paper
OOPSLA
DOI
Rapid: Region-Based Pointer Disambiguation
OOPSLA
DOI
Reference Capabilities for Flexible Memory Management
OOPSLA
DOI Pre-print
Regular Expression Matching using Bit Vector Automata
OOPSLA
DOI
Resource-Aware Soundness for Big-Step Semantics
OOPSLA
DOI
Reusing Just-in-Time Compiled Code
OOPSLA
DOI
Rhombus: A New Spin on Macros without All the Parentheses
OOPSLA
DOI Pre-print
Run-Time Prevention of Software Integration Failures of Machine Learning APIs
OOPSLA
DOI
Saggitarius: A DSL for Specifying Grammatical Domains
OOPSLA
DOI
Secure RDTs: Enforcing Access Control Policies for Offline Available JSON Data
OOPSLA
DOI Pre-print
Simple Reference Immutability for System F<:
OOPSLA
DOI
Solving Conditional Linear Recurrences for Program Verification: The Periodic Case
OOPSLA
DOI
Solving String Constraints with Lengths by StabilizationDistinguished Paper
OOPSLA
DOI
Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent MemoryDistinguished Paper
OOPSLA
DOI
Static Analysis of Memory Models for SMT Encodings
OOPSLA
DOI
Structural Subtyping as Parametric Polymorphism
OOPSLA
DOI Pre-print
Stuttering for Free
OOPSLA
DOI
Synthesizing Efficient Memoization Algorithms
OOPSLA
DOI
Synthesizing Precise Static Analyzers for Automatic Differentiation
OOPSLA
DOI
Synthesizing Specifications
OOPSLA
DOI
TASTyTruffle: Just-in-Time Specialization of Parametric Polymorphism
OOPSLA
DOI
The Bounded Pathwidth of Control-Flow Graphs
OOPSLA
DOI
The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog
OOPSLA
DOI
Towards Better Semantics Exploration for Browser Fuzzing
OOPSLA
DOI
Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs
OOPSLA
DOI Pre-print
Two Birds with One Stone: Boosting Code Generation and Code Search via a Generative Adversarial Network
OOPSLA
DOI Pre-print
Type-Safe Dynamic Placement with First-Class Placed Values
OOPSLA
DOI Pre-print
User-Customizable Transpilation of Scripting Languages
OOPSLA
DOI
Validating IoT Devices with Rate-Based Session Types
OOPSLA
DOI
Verification-Preserving Inlining in Automatic Separation Logic Verifiers
OOPSLA
DOI
Verifying Indistinguishability of Privacy-Preserving Protocols
OOPSLA
DOI
Verus: Verifying Rust Programs using Linear Ghost Types
OOPSLA
DOI
When Concurrency Matters: Behaviour-Oriented Concurrency
OOPSLA
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

  1. omit author names and institutions,
  2. use the third person when referencing your work,
  3. 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.