SPLASH 2023
Sun 22 - Fri 27 October 2023
Cascais, Portugal
Toggle navigation
Attending
Venue: Hotel Cascais Miragem
Registration
Sponsoring
Code of conduct
Support for Attending the Conference
Program
Complete Program
Your Program
Sun 22 Oct
Mon 23 Oct
Tue 24 Oct
Wed 25 Oct
Thu 26 Oct
Fri 27 Oct
Tracks
SPLASH 2023
Doctoral Symposium
OOPSLA
OOPSLA Artifacts
Onward! Essays
Onward! Papers
PLMW
Posters
SPLASH-E
Student Research Competition
Volunteers
Workshops
CARES
Co-hosted Conferences
DLS
GPCE
LOPSTR
MPLR
PPDP
SAS
SAS
SAS
SAS
Artifacts
SLE
Workshops
CONFLANG
23
FTSCS
HATRA
IWACO
LIVE
PAINT
PLF
REBLS
ST30
VMIL
VMIL
- Keynote
Organization
SPLASH 2023 Committees
Organizing Committee
Steering Committee
Track Committees
Doctoral Symposium
OOPSLA
OOPSLA Review Committee
External Review / Artifact Evaluation Committee
OOPSLA Artifacts
Onward! Essays
Program Committee
Onward! Steering Committee
Onward! Papers
Program Committee
Steering Committee
PLMW
Organizing Committee
Speakers & Panelists
Mentors
Posters
SPLASH-E
Program Commitee
Steering Committee
Student Research Competition
Organizers
Reviewers
Volunteers
Workshops
Contributors
People Index
Co-hosted Conferences
DLS
Program Committee
Steering Committee
GPCE
Organizing Committee
Program Committee
LOPSTR
N/A - check homepage
MPLR
Organizing Committee
Program Committee
PPDP
N/A - check homepage
SAS
Invited Speakers
Organizing Committee
SAS 2023
SAS 2023 Artifacts
SLE
Organizing Committee
Program Committee
Workshops
CONFLANG
Organizing Committee
Program Committee
FTSCS
Organizing Committee
Program Committee
HATRA
Organizing Committee
Program Committee
IWACO
Organizing Committee
Program Committee
LIVE
Organizing Committee
Program Committee
PAINT
Organizing Committee
Program Committee
PLF
Organizing Committee
Program Committee
REBLS
Organizing Committee
Program Committee
ST30
Organizing Committee
Programme Committee
VMIL
Organizing Committee
Program Committee
Search
Series
Series
SPLASH 2024
SPLASH 2023
SPLASH 2022
SPLASH 2021
SPLASH 2020
SPLASH 2019
SPLASH 2018
SPLASH 2017
SPLASH 2016
SPLASH 2015
SPLASH 2014
SPLASH 2013
SPLASH 2012
SPLASH 2011
SPLASH 2010
OOPSLA 2009
OOPSLA 2008
OOPSLA 2007
OOPSLA 2006
OOPSLA 2005
OOPSLA 2004
OOPSLA 2003
OOPSLA 2002
OOPSLA 2001
OOPSLA 2000
Sign in
Sign up
SPLASH 2023
(
series
) /
Hotel Cascais Miragem
/
Room information: Room I
Venue
Hotel Cascais Miragem
Room name
Room I
Floor
0
Capacity
392
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
This program is tentative and subject to change.
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT+01:00) Lisbon
.
Use conference time zone: (GMT+01:00) Lisbon
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-09:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-08:00) Alaska
(GMT-07:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-07:00) Pacific Time (US & Canada)
(GMT-06:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-05:00) Central Time (US & Canada)
(GMT-04:00) Eastern Time (US & Canada)
(GMT-04:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-03:00) Atlantic Time (Goose Bay)
(GMT-03:00) Atlantic Time (Canada)
(GMT-02:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-02:00) Miquelon, St. Pierre
(GMT-02:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT) Azores
(UTC) Coordinated Universal Time
(GMT+01:00) Belfast
(GMT+01:00) Dublin
(GMT+01:00) Lisbon
(GMT+01:00) London
(GMT) Monrovia, Reykjavik
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+02:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+03:00) Athens
(GMT+03:00) Beirut
(GMT+02:00) Cairo
(GMT+03:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+03:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
You're viewing the program in a time zone which is different from your device's time zone -
change time zone
Sun 22 Oct
Displayed time zone:
Lisbon
change
09:00 - 10:30
Session 1
PPDP
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 2
PPDP
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 3
PPDP
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 4
PPDP
at
Room I
16:00
30m
Paper
Type-directed Program Transformation for Constant-Time Enforcement
PPDP
Gautier Raimondi
Inria
,
Frédéric Besson
,
Thomas P. Jensen
INRIA Rennes
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 5
PPDP
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
11:00 - 12:30
Session 6
PPDP
at
Room I
11:00
90m
Talk
Unification modulo equational theories in languages with binding operators
PPDP
Maribel Fernandez
King's College London
14:00 - 15:30
Session 7
PPDP
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 8
PPDP
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
09:00 - 10:30
Keynote 1
OOPSLA
at
Room I
09:00
90m
Keynote
Scaling up machine learning without tears (and what do programming languages have to do with it)
Keynote
OOPSLA
Dimitrios Vytiniotis
DeepMind
11:00 - 12:30
AI4SE
OOPSLA
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
SE4AI
OOPSLA
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
probabilistic
OOPSLA
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
09:00 - 10:30
Keynote 2
OOPSLA
at
Room I
09:00
90m
Keynote
Hydroflow: A Compiler Target for Fast, Correct Distributed Programs
Keynote
OOPSLA
Joseph M. Hellerstein
UC Berkeley
11:00 - 12:30
type systems 1
OOPSLA
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 2
OOPSLA
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 systems
OOPSLA
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 3
OOPSLA
at
Room I
09:00
90m
Keynote
All the Languages Together
Keynote
OOPSLA
Amal Ahmed
Northeastern University, USA
11:00 - 12:30
verification 1
OOPSLA
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 2
OOPSLA
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 2
OOPSLA
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
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Room I
PPDP
Session 1
PPDP
Session 2
PPDP
Session 3
PPDP
Session 4
Mon 23 Oct
Displayed time zone:
Lisbon
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Room I
PPDP
Session 5
PPDP
Session 6
PPDP
Session 7
PPDP
Session 8
Wed 25 Oct
Displayed time zone:
Lisbon
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Room I
OOPSLA
Keynote 1
OOPSLA
AI4SE
OOPSLA
SE4AI
OOPSLA
probabilistic
Thu 26 Oct
Displayed time zone:
Lisbon
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Room I
OOPSLA
Keynote 2
OOPSLA
type systems 1
OOPSLA
type systems 2
OOPSLA
effect systems
Fri 27 Oct
Displayed time zone:
Lisbon
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Room I
OOPSLA
Keynote 3
OOPSLA
verification 1
OOPSLA
verification 2
OOPSLA
distribution & networking 2
Sun 22 Oct
Displayed time zone:
Lisbon
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Room I
PPDP
A Calculus of Delayed Reductions
09:00 - 09:30
PPDP
Typed Equivalence of Labeled Effect Handlers and Labeled Delimited Cont ...
09:30 - 10:00
PPDP
Comprehending queries over finite maps
10:00 - 10:30
PPDP
Embedding Quantitative Properties of Call-by-Name and Call-by-Value in ...
11:00 - 12:30
PPDP
Coq: the world's best macro assembler?
14:00 - 15:30
PPDP
Type-directed Program Transformation for Constant-Time Enforcement
16:00 - 16:30
PPDP
Data-Dependent Confidentiality in DCR Graphs
16:30 - 17:00
PPDP
---
17:00 - 17:30
Mon 23 Oct
Displayed time zone:
Lisbon
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Room I
PPDP
Multicompatibility for Multiparty-Session Composition
09:00 - 09:30
PPDP
Termination in Concurrency, Revisited
09:30 - 10:00
PPDP
Polymorphic Typestate for Session Types
10:00 - 10:30
PPDP
Unification modulo equational theories in languages with binding operators
11:00 - 12:30
PPDP
Strongly-Typed Multi-View Stack-Based Computations
14:00 - 14:30
PPDP
Closure Conversion in Little Pieces
14:30 - 15:00
PPDP
Additive Cellular Automata Graded-Monadically
15:00 - 15:30
PPDP
Intuitionistic Metric Temporal Logic
16:00 - 16:30
PPDP
stablekanren: Integrating Stable Model Semantics with miniKanren
16:30 - 17:00
PPDP
Closing of PPDP
17:00 - 17:30
Wed 25 Oct
Displayed time zone:
Lisbon
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Room I
SPLASH OOPSLA
Keynote
Scaling up machine learning without tears (and what do programming lang ...
09:00 - 10:30
SPLASH OOPSLA
Grounded Copilot: How Programmers Interact with Code-Generating Models
11:00 - 11:18
SPLASH OOPSLA
Two Birds with One Stone: Boosting Code Generation and Code Search via ...
11:18 - 11:36
SPLASH OOPSLA
Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates ...
11:36 - 11:54
SPLASH OOPSLA
Concrete Type Inference for Code Optimization Using Machine Learning wi ...
11:54 - 12:12
SPLASH OOPSLA
An Explanation Method for Models of Code
12:12 - 12:30
SPLASH OOPSLA
Deep Learning Robustness Verification for Few-Pixel Attacks
14:00 - 14:18
SPLASH OOPSLA
Run-Time Prevention of Software Integration Failures of Machine Learnin ...
14:18 - 14:36
SPLASH OOPSLA
Compiling Structured Tensor Algebra
14:36 - 14:54
SPLASH OOPSLA
Perception Contracts for Safety of ML-Enabled Systems
14:54 - 15:12
SPLASH OOPSLA
Languages with Decidable Learning: A Meta-theorem
15:12 - 15:30
SPLASH OOPSLA
A Deductive Verification Infrastructure for Probabilistic Programs
16:00 - 16:18
SPLASH OOPSLA
A Gradual Probabilistic Lambda Calculus
16:18 - 16:36
SPLASH OOPSLA
Lower Bounds for Possibly Divergent Probabilistic Programs
16:36 - 16:54
SPLASH OOPSLA
Exact Recursive Probabilistic Programming
16:54 - 17:12
SPLASH OOPSLA
Solving String Constraints with Lengths by Stabilization
17:12 - 17:30
Thu 26 Oct
Displayed time zone:
Lisbon
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Room I
SPLASH OOPSLA
Keynote
Hydroflow: A Compiler Target for Fast, Correct Distributed Programs
09:00 - 10:30
SPLASH OOPSLA
Reference Capabilities for Flexible Memory Management
11:00 - 11:18
SPLASH OOPSLA
A Grounded Conceptual Model for Ownership Types in Rust
11:18 - 11:36
SPLASH OOPSLA
Inference of Resource Management Specifications
11:36 - 11:54
SPLASH OOPSLA
Resource-aware soundness for big-step semantics
11:54 - 12:12
SPLASH OOPSLA
Verus: Verifying Rust Programs using Linear Ghost Types
12:12 - 12:30
SPLASH OOPSLA
Greedy Implicit Bounded Quantification
14:00 - 14:18
SPLASH OOPSLA
Structural Subtyping as Parametric Polymorphism
14:18 - 14:36
SPLASH OOPSLA
Simple Reference Immutability for System F-Sub
14:36 - 14:54
SPLASH OOPSLA
Mutually Iso-recursive Subtyping
14:54 - 15:12
SPLASH OOPSLA
Getting Into The Flow: Better Type Error Messages for Constraint-Based ...
15:12 - 15:30
SPLASH OOPSLA
Fast and Efficient Boolean Unification for Hindley-Milner-Style Type an ...
16:00 - 16:18
SPLASH OOPSLA
From Capabilities to Regions: Enabling Efficient Compilation of Lexical ...
16:18 - 16:36
SPLASH OOPSLA
Gradual Typing for Effect Handlers
16:36 - 16:54
SPLASH OOPSLA
When Concurrency Matters: Behaviour-Oriented Concurrency
16:54 - 17:12
SPLASH OOPSLA
Continuing WebAssembly with Effect Handlers
17:12 - 17:30
Fri 27 Oct
Displayed time zone:
Lisbon
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Room I
SPLASH OOPSLA
Keynote
All the Languages Together
09:00 - 10:30
SPLASH OOPSLA
Solving Conditional Linear Recurrences for Program Verification: The Pe ...
11:00 - 11:18
SPLASH OOPSLA
Melocoton: A Program Logic for Verified Interoperability Between OCaml ...
11:18 - 11:36
SPLASH OOPSLA
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness ...
11:36 - 11:54
SPLASH OOPSLA
Formal Abstractions for Packet Scheduling
11:54 - 12:12
SPLASH OOPSLA
P4R-Type: a Verified API for P4 Control Plane Programs
12:12 - 12:30
SPLASH OOPSLA
Stuttering for Free
14:00 - 14:18
SPLASH OOPSLA
Compositional Verification of Efficient Masking Countermeasures against ...
14:18 - 14:36
SPLASH OOPSLA
Generating Proof Certificates for a Language-Agnostic Deductive Program ...
14:36 - 14:54
SPLASH OOPSLA
Complete First-Order Reasoning for Properties of Functional Programs
14:54 - 15:12
SPLASH OOPSLA
Counterexample Driven Quantifier Instantiations with Applications to Di ...
15:12 - 15:30
SPLASH OOPSLA
Hybrid Multiparty Session Types: Compositionality for Protocol Specific ...
16:00 - 16:18
SPLASH OOPSLA
Mechanizing Session-Types Using a Structural View: Enforcing linearity ...
16:18 - 16:36
SPLASH OOPSLA
Message Chains for Distributed System Verification
16:36 - 16:54
SPLASH OOPSLA
Randomized Testing of Byzantine Fault Tolerant Algorithms
16:54 - 17:12
SPLASH OOPSLA
Validating IoT Devices with Rate-Based Session Types
17:12 - 17:30
x
Wed 4 Oct 16:02