SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025

This program is tentative and subject to change.

Thu 16 Oct 2025 11:30 - 11:45 at Orchid West - Theory

The merge operator is a powerful construct in programming languages, enabling flexible composition of various components such as functions, records, or classes. Unfortunately, its application often leads to ambiguity and non-determinism, especially when dealing with overlapping types. To prevent ambiguity, approaches such as disjoint intersection types have been proposed. However, disjointness imposes strict constraints to ensure determinism, at the cost of limiting expressiveness, particularly for function overloading. This paper introduces a novel concept called \emph{type apartness}, which relaxes the strict disjointness constraints, while maintaining type safety and determinism. Type apartness allows some overlap between types as long as overlapping parts can be \emph{distinguished through specific upcasts}. By further incorporating the notion of guarded subtyping to prevent ambiguity when upcasting, our approach is the first to support \emph{function overloading}, \emph{return type overloading}, \emph{extensible records}, and \emph{nested composition} all at once in a single calculus while preserving determinism. We formalize our calculi and proofs using Coq and prove their type soundness and determinism. Additionally, we demonstrate how type normalization and type difference can be used to ensure consistency and resolve conflicts, enhancing the flexibility and expressiveness of the merge operator.

This program is tentative and subject to change.

Thu 16 Oct

Displayed time zone: Perth change

10:30 - 12:15
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 TU Wien, Vienna, Austria, 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
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