OOPSLASPLASH 2023
This program is tentative and subject to change.
Wed 25 OctDisplayed time zone: Lisbon change
09:00 - 10:30 | |||
09:00 90mKeynote | Scaling up machine learning without tears (and what do programming languages have to do with it) OOPSLA Dimitrios Vytiniotis DeepMind |
10:30 - 11:00 | |||
11:00 - 12:30 | |||
11:00 18mTalk | 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 18mTalk | 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 | ||
11:36 18mTalk | Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs OOPSLA Alex Renda Massachusetts Institute of Technology, Yi Ding Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology Pre-print | ||
11:54 18mTalk | 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 | ||
12:12 18mTalk | An Explanation Method for Models of Code OOPSLA |
11:00 - 12:30 | |||
11:00 18mTalk | 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 IST Austria, Austria, S. Hitarth Hong Kong University of Science and Technology | ||
11:18 18mTalk | Equality Saturation Theory Exploration à la Carte OOPSLA Anjali Pal University of Washington, Brett Saiki University of Washington, Oliver Flatt , Ryan Tjoa University of Washington, Amy Zhu University of Washington, Cynthia Richey University of Washington, Max Willsey University of California, Berkeley, Zachary Tatlock University of Washington, Chandrakana Nandi Certora Pre-print | ||
11:36 18mTalk | Synthesizing Specifications OOPSLA Kanghee Park University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison | ||
11:54 18mTalk | 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 | ||
12:12 18mTalk | 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 |
14:00 - 15:30 | |||
14:00 18mTalk | Deep Learning Robustness Verification for Few-Pixel Attacks OOPSLA DOI | ||
14:18 18mTalk | 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 University of Chicago | ||
14:36 18mTalk | 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 | ||
14:54 18mTalk | Perception Contracts for Safety of ML-Enabled Systems OOPSLA Angello Astorga University of Illinois at Urbana-Champaign, Chiao Hsieh Graduate School of Informatics, Kyoto University, P. Madhusudan University of Illinois at Urbana-Champaign, Sayan Mitra University of Illinois at Urbana-Champaign | ||
15:12 18mTalk | 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 |
14:00 - 15:30 | |||
14:00 18mTalk | 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 | ||
14:18 18mTalk | Data Extraction via Semantic Regular Expression Synthesis OOPSLA Qiaochu Chen University of Texas at Austin, Arko Banerjee University of Texas at Austin, Çağatay Demiralp MIT CSAIL, Greg Durrett University of Texas at Austin, Işil Dillig University of Texas at Austin | ||
14:36 18mTalk | Synthesizing Efficient Memoization Algorithms OOPSLA | ||
14:54 18mTalk | 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 18mTalk | Modular Component-Based Quantum Circuit Synthesis OOPSLA DOI |
15:30 - 16:00 | |||
16:00 - 17:30 | |||
16:00 18mTalk | 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 | ||
16:18 18mTalk | 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 18mTalk | 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 DOI | ||
16:54 18mTalk | 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 18mTalk | Solving String Constraints with Lengths by Stabilization OOPSLA Yu-Fang Chen Academia Sinica, Taiwan, David Chocholatý Brno University of Technology, Czech Republic, 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, Czech Republic |
16:00 - 17:30 | |||
16:00 15mTalk | Fluent APIs in Functional Languages OOPSLA DOI Pre-print | ||
16:15 15mTalk | 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 Nanjing University, Wenguang Chen Tsinghua University | ||
16:30 15mTalk | How Domain Experts Use an Embedded DSL OOPSLA | ||
16:45 15mTalk | 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 | ||
17:00 15mTalk | A Pretty Expressive Printer OOPSLA Sorawee Porncharoenwase University of Washington, Justin Pombrio Brown University, USA, Emina Torlak Amazon Web Services and University of Washington Pre-print | ||
17:15 15mTalk | 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 |
Thu 26 OctDisplayed time zone: Lisbon change
09:00 - 10:30 | |||
09:00 90mKeynote | Thursday Keynote (Title Placeholder) OOPSLA Joseph M. Hellerstein UC Berkeley |
10:30 - 11:00 | |||
11:00 - 12:30 | |||
11:00 18mTalk | Reference Capabilities for Flexible Memory Management OOPSLA Ellen Arvidsson Uppsala University, Elias Castegren Uppsala University, Sylvan Clebsch Azure Research, Sophia Drossopoulou Imperial College London , James Noble Research & Programming, Matthew Parkinson Azure Research, Microsoft, UK, Tobias Wrigstad Uppsala University, Sweden | ||
11:18 18mTalk | A Grounded Conceptual Model for Ownership Types in Rust OOPSLA Will Crichton Brown University, Gavin Gray ETH Zürich, Shriram Krishnamurthi Brown University, United States DOI Pre-print | ||
11:36 18mTalk | Inference of Resource Management Specifications OOPSLA Narges Shadab University of California at Riverside, PRITAM MANOHAR GHARAT Microsoft Research India, 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 | ||
11:54 18mTalk | 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 | ||
12:12 18mTalk | 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 | |||
11:00 18mTalk | 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 | ||
11:18 18mTalk | Regular Expression Matching using Bit Vector Automata OOPSLA Alexis Le Glaunec Rice University, Lingkun Kong Rice University, Konstantinos Mamouras Rice University DOI | ||
11:36 18mTalk | 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 18mTalk | Bring Your Own Data Structures to Datalog OOPSLA Arash Sahebolamri Syracuse University, Langston Barrett Galois, Inc, Scott Moore Galois, Inc., Kristopher Micinski Syracuse University | ||
12:12 18mTalk | Rhombus: A New Spin on Macros Without All the Parentheses OOPSLA Matthew Flatt University of Utah, Taylor Allred University of Utah, Ross Angle independent, Stephen De Gabrielle independent, Robby Findler Northwestern University, Jack Firth independent, Kiran Gopinathan National University of Singapore, Ben Greenman Brown University, Siddhartha Kasivajhula independent, Alex Knauth Northeastern University, Jay McCarthy University of Massachusetts Lowell & Reach, Sam Phillips independent, Sorawee Porncharoenwase University of Washington, Jens Axel Søgaard independent, Sam Tobin-Hochstadt Indiana University Pre-print |
14:00 - 15:30 | |||
14:00 18mTalk | 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 | ||
14:18 18mTalk | Structural Subtyping as Parametric Polymorphism OOPSLA Wenhao Tang The University of Edinburgh, Daniel Hillerström Huawei Zurich Research Center, James McKinna Heriot-Watt University, Michel Steuwer Technische Universität Berlin / University of Edinburgh, Ornela Dardha University of Glasgow, Rongxiao Fu The University of Edinburgh, Sam Lindley University of Edinburgh | ||
14:36 18mTalk | Simple Reference Immutability for System F-Sub OOPSLA | ||
14:54 18mTalk | Mutually Iso-recursive Subtyping OOPSLA Andreas Rossberg Independent | ||
15:12 18mTalk | Getting Into The Flow: Better Type Error Messages for Constraint-Based Type Inference OOPSLA Ishan Bhanuka HKUST (The Hong Kong University of Science and Technology), Lionel Parreaux HKUST (The Hong Kong University of Science and Technology), David Binder University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen |
14:00 - 15:30 | |||
14:00 18mTalk | The Bounded Pathwidth of Control-flow Graphs OOPSLA Giovanna Kobus Conrado Hong Kong University of Science and Technology (HKUST), Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Chun Kit LAM Hong Kong University of Science and Technology (HKUST) | ||
14:18 18mTalk | How Profilers Can Help Navigate Type Migration OOPSLA Ben Greenman Brown University, Matthias Felleisen PLT @ Northeastern University, Christos Dimoulas PLT @ Northwestern University | ||
14:36 18mTalk | 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, Gagandeep Singh University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-Champaign | ||
14:54 18mTalk | A Container-Usage-Pattern-based Context Debloating Approach for Object-Sensitive Pointer Analysis OOPSLA Dongjie He UNSW, Yujiang Gui UNSW Sydney, Wei Li University of New South Wales, Yonggang Tao University of New South Wales, Changwei Zou University of New South Wales, Yulei Sui University of New South Wales, Sydney, Jingling Xue UNSW | ||
15:12 18mTalk | Static Analysis of Memory Models for SMT Encodings OOPSLA Thomas Haas Technical University of Braunschweig, René Maseli TU Braunschweig, Roland Meyer TU Braunschweig, Hernán Ponce de León Huawei Dresden Research Center |
15:30 - 16:00 | |||
16:00 - 17:30 | |||
16:00 18mTalk | 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, Denmark | ||
16:18 18mTalk | 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 | ||
16:36 18mTalk | Gradual Typing for Effect Handlers OOPSLA Max New University of Michigan, Eric Giovannini University of Michigan, Dan Licata Wesleyan University | ||
16:54 18mTalk | When Concurrency Matters: Behaviour-Oriented Concurrency OOPSLA Luke Cheeseman Imperial College London, Matthew Parkinson Azure Research, Microsoft, UK, Sylvan Clebsch Azure Research, Marios Kogias Imperial College London & Microsoft Research, Sophia Drossopoulou Imperial College London , David Chisnall , Tobias Wrigstad Uppsala University, Sweden, Paul Liétar Imperial College London | ||
17:12 18mTalk | Continuing WebAssembly with Effect Handlers OOPSLA Luna Phipps-Costin Northeastern University, Andreas Rossberg Independent, Arjun Guha Northeastern University and Roblox Research, Daan Leijen Microsoft Research, Daniel Hillerström Huawei Zurich Research Center, KC Sivaramakrishnan IIT Madras and Tarides, Matija Pretnar University of Ljubljana, Slovenia, Sam Lindley University of Edinburgh Pre-print |
16:00 - 17:30 | |||
16:00 18mTalk | Historia: Refuting Callback Reachability with Message-History Logics OOPSLA Shawn Meier University of Colorado, Boulder, Sergio Mover Ecole Polytechnique, Gowtham Kaki University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon | ||
16:18 18mTalk | 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 (HKUST), 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 HKUST | ||
16:36 18mTalk | A Cocktail Approach to Practical Call Graph Construction OOPSLA Yuandao Cai Hong Kong University of Science and Technology, China, Charles Zhang Hong Kong University of Science and Technology | ||
16:54 18mTalk | 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 | ||
17:12 18mTalk | 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 | |||
16:00 18mTalk | 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 Computer and Cyber Sciences, Augusta University, Georgia, USA, Tiark Rompf Purdue University | ||
16:18 18mTalk | 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 18mTalk | Reusing Just-in-Time Compiled Code OOPSLA Meetesh Kalpesh Mehta Indian Institute of Technology Bombay, Sebastián Krynski Czech Technical University, Hugo Musso Gualandi Czech Technical University in Prague, Manas Thakur Indian Institute of Technology Bombay, Jan Vitek Northeastern University | ||
16:54 18mTalk | 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 | ||
17:12 18mTalk | 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 Georgia Institute of Technology, USA, Ada Gavrilovska Georgia Institute of Technology, Santosh Pande Georgia Institute of Technology |
Fri 27 OctDisplayed time zone: Lisbon change
09:00 - 10:30 | |||
09:00 90mTalk | Friday Keynote (Title Placeholder) OOPSLA Amal Ahmed Northeastern University, USA |
10:30 - 11:00 | |||
11:00 - 12:30 | |||
11:00 15mTalk | 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, China | ||
11:30 15mTalk | 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:45 15mTalk | Interactive Debugging of Datalog Programs OOPSLA | ||
12:00 15mTalk | Accelerating Fuzzing through Prefix-Guided Execution OOPSLA DOI | ||
12:15 15mTalk | MemPerf: Profiling Allocator-Induced Performance Slowdowns OOPSLA Jin Zhou University of Massachusetts Amherst, Sam Silvestro University of Texas at San Antonio, Jiaxun,Tang University of Massachusetts Amherst, Hanmei Yang University of Massachusetts Amherst, Hongyu Liu University of Texas at San Antonio, Guangming Zeng Synopsys, Bo Wu Colorado School of Mines, Cong Liu University of California at Riverside, Tongping Liu University of Massachusetts at Amherst |
14:00 - 15:30 | |||
14:00 18mTalk | Stuttering for Free OOPSLA Minki Cho Seoul National University, Youngju Song MPI-SWS, Dongjae Lee Seoul National University, Lennard Gäher MPI-SWS & Saarland University, Derek Dreyer MPI-SWS | ||
14:18 18mTalk | Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks OOPSLA Pengfei Gao ShanghaiTech University, Yedi Zhang ShanghaiTech University, Fu Song ShanghaiTech University, Taolue Chen Birkbeck University of London, Francois-Xavier Standaert UCLouvain | ||
14:36 18mTalk | 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:54 18mTalk | Complete First-Order Reasoning for Properties of Functional Programs OOPSLA Adithya Murali University of Illinois at Urbana-Champaign, Lucas Pena , Ranjit Jhala University of California at San Diego, P. Madhusudan University of Illinois at Urbana-Champaign | ||
15:12 18mTalk | Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols OOPSLA Orr Tamir Tel Aviv University, Marcelo Taube Tel Aviv University, Israel, Kenneth L. McMillan University of Texas at Austin, Sharon Shoham Tel Aviv University, Jon Howell VMware Research, Guy Gueta VMWare, Mooly Sagiv Tel Aviv University |
14:00 - 15:30 | |||
14:00 15mTalk | 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:15 15mTalk | Rapid: Region-based Pointer Disambiguation OOPSLA | ||
14:30 15mTalk | Automated Ambiguity Detection in Layout-Sensitive Grammars OOPSLA Jiangyi Liu Tsinghua University, Fengmin Zhu CISPA Helmholtz Center for Information Security, Fei He Tsinghua University Pre-print | ||
14:45 15mTalk | Formally Verifying Optimizations with Block Simulations OOPSLA Leo Gourdin Université Grenoble-Alpes, Benjamin Bonneau ENS PSL, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David Monniaux CNRS/VERIMAG, Alexandre Bérard Université Grenoble-Alpes DOI Pre-print | ||
15:00 15mTalk | Hardware-Aware Static Optimization of Hyperdimensional Computations OOPSLA |
15:30 - 16:00 | |||
16:00 - 17:30 | |||
16:00 18mTalk | 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 18mTalk | Adventure of a Lifetime: Extract Method Refactoring for Rust OOPSLA Sewen Thy Ahrefs Research, Andreea Costea School of Computing, National University Of Singapore, Kiran Gopinathan National University of Singapore, Ilya Sergey National University of Singapore DOI Pre-print | ||
16:36 18mTalk | Inductive Program Synthesis Guided by Observational Program Similarity OOPSLA John Feser Massachusetts Institute of Technology, Işil Dillig University of Texas at Austin, Armando Solar-Lezama Massachusetts Institute of Technology | ||
16:54 18mTalk | 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şil Dillig University of Texas at Austin DOI | ||
17:12 18mTalk | 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 | |||
16:00 18mTalk | Verification-Preserving Inlining in Automatic Separation Logic Verifiers OOPSLA DOI | ||
16:18 18mTalk | Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory OOPSLA | ||
16:36 18mTalk | 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 | ||
16:54 18mTalk | Proof Automation for Linearizability in Separation Logic OOPSLA DOI Pre-print | ||
17:12 18mTalk | Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic OOPSLA Jaehwang Jung KAIST, South Korea, Janggun Lee KAIST, Jaemin Choi , Jaewoo Kim KAIST, Sunho Park KAIST, Jeehoon Kang KAIST |
Accepted Papers
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.
Information for Reviewers
Important dates
-
2023-04-19 – Quick expertise check.
-
2023-04-24 – Start of the review phase.
- 2023-05-08 – 30% of papers due.
- 2023-05-22 – 60% of papers due.
- 2023-06-09 – All reviews due.
-
2023-06-16 – Start of asynchronous discussions (2 weeks).
- 2023-06-28 + 2023-06-29, 14:00-18:00 UTC – potential sync meetings
- 2023-06-30 – Author notification.
-
2023-08-13 – Revision check for conditional accepts (2 weeks).
- 2023-08-27 – Final author notification.
Assignments: TPMS for initial assignment; you quickly scan assigned papers to judge the expertise and possibly suggest external reviewers; we use the information to reassign papers, if necessary.
Reviews: Please hand in reviews in the batches indicated by the timeline. Discussions after author response will happen mostly asynchronously. Only in case of disagreement will there be a synchronous discussion only for undecided papers.