SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
VenueHotel Cascais Miragem
Room nameRoom I
Floor0
Capacity392
Room InformationNo extra information available
Program

This program is tentative and subject to change.

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

Sun 22 Oct

Displayed time zone: Lisbon change

09:00 - 10:30
Session 1PPDP at Room I
09:00
30m
Paper
A Calculus of Delayed Reductions
PPDP
Steffen van Bakel , Nicolas Wu Imperial College London, Emma Tye
09:30
30m
Paper
Typed Equivalence of Labeled Effect Handlers and Labeled Delimited Control Operators
PPDP
Kazuki Ikemori Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology
10:00
30m
Paper
Comprehending queries over finite maps
PPDP
Wilmer Ricciotti University of Edinburgh, UK
11:00 - 12:30
Session 2PPDP at Room I
11:00
90m
Talk
Embedding Quantitative Properties of Call-by-Name and Call-by-Value in a Unified Framework
PPDP
Delia Kesner Université Paris Cité - CNRS - IRIF; Institut Universitaire de France
14:00 - 15:30
Session 3PPDP at Room I
14:00
90m
Talk
Coq: the world's best macro assembler?
PPDP
Andrew Kennedy Facebook London, Nick Benton Microsoft Research, Cambridge, Jonas Jensen Semmle, Pierre-Evariste Dagand IRIF / CNRS
16:00 - 17:30
Session 4PPDP at Room I
16:00
30m
Paper
Type-directed Program Transformation for Constant-Time Enforcement
PPDP
16:30
30m
Paper
Data-Dependent Confidentiality in DCR Graphs
PPDP
Eduardo Geraldo , João Costa Seco NOVA-LINCS; Nova University of Lisbon, Thomas T. Hildebrandt University of Copenhagen
17:00
30m
Break
---
PPDP

Mon 23 Oct

Displayed time zone: Lisbon change

09:00 - 10:30
Session 5PPDP at Room I
09:00
30m
Paper
Multicompatibility for Multiparty-Session Composition
PPDP
Franco Barbanera , Mariangiola Dezani Università di Torino, Lorenzo Gheri University of Oxford, Nobuko Yoshida University of Oxford
09:30
30m
Paper
Termination in Concurrency, Revisited
PPDP
Joseph Paulus , Daniele Nantes-Sobrinho Imperial College London, Jorge A. Pérez University of Groningen
10:00
30m
Paper
Polymorphic Typestate for Session Types
PPDP
Hannes Saffrich University of Freiburg, Peter Thiemann University of Freiburg, Germany
14:00 - 15:30
Session 7PPDP at Room I
14:00
30m
Paper
Strongly-Typed Multi-View Stack-Based Computations
PPDP
Pieter Koopman Radboud University Nijmegen, Netherlands, Mart Lubbers Radboud University Nijmegen
14:30
30m
Paper
Closure Conversion in Little Pieces
PPDP
Zachary Sullivan University of Oregon, Paul Downen University of Massachusetts Lowell, Zena M. Ariola University of Oregon
15:00
30m
Paper
Additive Cellular Automata Graded-Monadically
PPDP
Silvio Capobianco , Tarmo Uustalu Reykjavik University
16:00 - 17:30
Session 8PPDP at Room I
16:00
30m
Paper
Intuitionistic Metric Temporal Logic
PPDP
Luiz de Sá , Bernardo Toninho NOVA-LINCS; Nova University of Lisbon, Frank Pfenning Carnegie Mellon University, USA
16:30
30m
Paper
stablekanren: Integrating Stable Model Semantics with miniKanren
PPDP
Xiangyu Guo Arizona State University, James Smith , Ajay Bansal
17:00
30m
Break
Closing of PPDP
PPDP

Wed 25 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
AI4SEOOPSLA at Room I
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
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
18m
Talk
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
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
12:12
18m
Talk
An Explanation Method for Models of Code
OOPSLA
Yu WANG Nanjing University, Ke Wang Visa Research, Linzhang Wang Nanjing University
14:00 - 15:30
SE4AIOOPSLA at Room I
14:00
18m
Talk
Deep Learning Robustness Verification for Few-Pixel Attacks
OOPSLA
Yuval Shapira Technion, Eran Avneri Technion, Dana Drachsler Cohen Technion
DOI
14:18
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 University of Chicago
14:36
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
14:54
18m
Talk
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
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
16:00 - 17:30
probabilisticOOPSLA at Room I
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
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
DOI
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, 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

Thu 26 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
type systems 1OOPSLA at Room I
11:00
18m
Talk
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
18m
Talk
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
18m
Talk
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
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
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
14:00 - 15:30
type systems 2OOPSLA at Room I
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
14:18
18m
Talk
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
Pre-print
14:36
18m
Talk
Simple Reference Immutability for System F-Sub
OOPSLA
Edward Lee University of Waterloo, Ondřej Lhoták University of Waterloo
14:54
18m
Talk
Mutually Iso-recursive Subtyping
OOPSLA
Andreas Rossberg Independent
15:12
18m
Talk
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
16:00 - 17:30
effect systemsOOPSLA at Room I
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, Denmark
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
Pre-print
16:36
18m
Talk
Gradual Typing for Effect Handlers
OOPSLA
Max New University of Michigan, Eric Giovannini University of Michigan, Dan Licata Wesleyan University
16:54
18m
Talk
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
18m
Talk
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

Fri 27 Oct

Displayed time zone: Lisbon change

09:00 - 10:30
Keynote 3OOPSLA at Room I
09:00
90m
Keynote
All the Languages TogetherKeynote
OOPSLA
Amal Ahmed Northeastern University, USA
11:00 - 12:30
verification 1OOPSLA at Room I
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 , Johannes Hostert Saarland University, MPI-SWS, Simon Spies MPI-SWS, Michael Sammler MPI-SWS, Lars Birkedal Aarhus University, Derek Dreyer MPI-SWS
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 Universiteit of the Netherlands and ILLC, University of Amsterdam, Dexter Kozen Cornell University
12:12
18m
Talk
P4R-Type: a Verified API for P4 Control Plane Programs
OOPSLA
Roberto Guanciale KTH, Alceste Scalas Technical University of Denmark, Philipp Haller KTH Royal Institute of Technology, Jens Kanstrup Larsen DTU
DOI Pre-print Media Attached
14:00 - 15:30
verification 2OOPSLA at Room I
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 & Saarland University, Derek Dreyer MPI-SWS
14:18
18m
Talk
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
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:54
18m
Talk
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
18m
Talk
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
16:00 - 17:30
distribution & networking 2OOPSLA at Room I
16:00
18m
Talk
Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection
OOPSLA
Lorenzo Gheri University of Oxford, 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
16:36
18m
Talk
Message Chains for Distributed System Verification
OOPSLA
Federico Mora University of California, Berkeley, Ankush Desai Amazon Web Services, Elizabeth Polgreen University of Edinburgh, Sanjit A. Seshia University of California, Berkeley
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

Sun 22 Oct

Displayed time zone: Lisbon change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Room I

Mon 23 Oct

Displayed time zone: Lisbon change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Room I

Wed 25 Oct

Displayed time zone: Lisbon change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Room I

Thu 26 Oct

Displayed time zone: Lisbon change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Room I

Fri 27 Oct

Displayed time zone: Lisbon change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Room I

Wed 25 Oct

Displayed time zone: Lisbon change

Fri 27 Oct

Displayed time zone: Lisbon change