SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Thu 16 Oct 2025 10:45 - 11:00 at Orchid West - Theory Chair(s): Lionel Parreaux

Choreographic programming is a promising new paradigm for programming concurrent systems where a developer writes a single centralized program that compiles to individual programs for each node. Existing choreographic languages, however, lack critical features integral to modern systems, like the ability of one node to dynamically compute who should perform a computation and send that decision to others. This work addresses this gap with $\lambda_\text{QC}$, the first typed choreographic language with first class process names and polymorphism over both types and (sets of) locations. $\lambda_\text{QC}$ also improves expressive power over previous work by supporting algebraic and recursive data types as well as multiply-located values. We formalize and mechanically verify our results in Rocq, including the standard choreographic guarantee of deadlock freedom.

Thu 16 Oct

Displayed time zone: Perth change

10:30 - 12:15
TheoryOOPSLA at Orchid West
Chair(s): Lionel Parreaux HKUST (The Hong Kong University of Science and Technology)
10:30
15m
Talk
Automated Discovery of Tactic Libraries for Interactive Theorem Proving
OOPSLA
Yutong Xin The University of Texas at Austin, Jimmy Xin The University of Texas at Austin, Gabriel Poesia Stanford University, Noah D. Goodman Stanford University, Jocelyn Qiaochu Chen New York University, University of Alberta, Işıl Dillig University of Texas at Austin
10:45
15m
Talk
Choreographic Quick Changes: First-Class Location (Set) Polymorphism
OOPSLA
Ashley Samuelson University of Wisconsin-Madison, Andrew K. Hirsch University at Buffalo, SUNY, Ethan Cecchetti University of Wisconsin-Madison
11:00
15m
Talk
Divide and Conquer: A Compositional Approach to Game-Theoretic Security
OOPSLA
Ivana Bocevska TU Wien, Anja Petković Komel Argot Collective, Laura Kovács TU Wien, Sophie Rain Argot Collective, Michael Rawson University of Southampton
11:15
15m
Talk
Efficient Decrease-And-Conquer Linearizability Monitoring
OOPSLA
Zheng Han Lee National University of Singapore, Singapore, Umang Mathur National University of Singapore
Link to publication DOI Pre-print
11:30
15m
Talk
Liberating Merges via Apartness and Guarded Subtyping
OOPSLA
Han Xu Princeton University, Xuejing Huang IRIF, Bruno C. d. S. Oliveira University of Hong Kong
11:45
15m
Talk
The Simple Essence of Monomorphization
OOPSLA
Matthew Lutze Aarhus University, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen
12:00
15m
Talk
What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
OOPSLA
Yichen Xu EPFL, Oliver Bračevac EPFL, LAMP, Nguyen Pham EPFL, LAMP, Martin Odersky EPFL
Pre-print