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

Monomorphization is a common implementation technique for parametric type-polymorphism, which avoids the potential runtime overhead of uniform representations at the cost of code duplication. While important as a folklore implementation technique, there is a lack of general formal treatments in the published literature. Moreover, it is commonly believed to be incompatible with higher-rank polymorphism. In this paper, we formally present a simple monomorphization technique based on a type-based flow analysis that generalizes to programs with higher-rank types, existential types, and arbitrary combinations. Inspired by algebraic subtyping, we track the flow of type instantiations through the program. Our approach only supports monomorphization up to polymorphic recursion, which we uniformly detect as cyclic flow. Treating universal and existential quantification uniformly, we identify a novel form of polymorphic recursion in the presence of existential types, which we coin polymorphic packing. We study the meta-theory of our approach, showing that our translation is type-preserving and preserves semantics step-wise.

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