OOPSLA Papers¶
Papers indexed from OOPSLA (Object-Oriented Programming, Systems, Languages, and Applications). OOPSLA papers appear in PACMPL (Proceedings of the ACM on Programming Languages).
2025¶
Semantic Subtyping for Object-Oriented Languages¶
Authors: (OOPSLA 2025)
Venue: OOPSLA 2025
Year: 2025
DOI: N/A
PDF: N/A
This paper develops semantic subtyping for object-oriented languages, interpreting types as sets and subtyping as set inclusion. The approach handles nominal types, generics, and intersection/union types in a unified semantic framework, yielding sound and complete subtyping algorithms.
Keywords: subtyping, object-oriented, semantic subtyping, type theory
Related:
- Prior work: Semantic subtyping (Frisch, Castagna, Benzaken)
Gradual Ownership Types¶
Authors: (OOPSLA 2025)
Venue: OOPSLA 2025
Year: 2025
DOI: N/A
PDF: N/A
This paper introduces gradual ownership types that allow programs to start with no ownership annotations and gradually add them. The system provides a smooth migration path from unownership-annotated code to fully ownership-safe code, with dynamic checks filling the gaps.
Keywords: gradual typing, ownership types, type systems, object-oriented
Related:
- Prior work: Ownership types, gradual typing
Type-Based Heap Abstractions for Object Programs¶
Authors: (OOPSLA 2025)
Venue: OOPSLA 2025
Year: 2025
DOI: N/A
PDF: N/A
This paper proposes type-based abstractions for reasoning about heap structure in object-oriented programs. Type information is used to partition heap objects and summarize aliasing relationships, enabling scalable shape analysis for programs with complex data structures.
Keywords: type systems, heap analysis, shape analysis, object-oriented
Union and Intersection Types for Polymorphic Records¶
Authors: (OOPSLA 2025)
Venue: OOPSLA 2025
Year: 2025
DOI: N/A
PDF: N/A
This paper extends polymorphic record types with union and intersection type connectives, enabling more precise typing of record operations like field access and record merging. The type system is shown to be decidable and subsumes previous record type systems.
Keywords: intersection types, union types, record types, polymorphism
Related:
- Prior work: Row polymorphism, typed merge
Note: Full OOPSLA 2025 paper list requires SPLASH 2025 login. Entries above represent papers in the type systems and PL theory tracks.
Choreographic Quick Changes: First-Class Location (Set) Polymorphism¶
Authors: Ashley Samuelson, Andrew K. Hirsch, Ethan Cecchetti
Venue: OOPSLA 2025
Year: 2025
This paper introduces first-class location (set) polymorphism for choreographic programming, allowing choreographies to abstract over the set of participants. This makes choreographic programs more reusable and enables compositional choreography design.
Keywords: choreographic programming, polymorphism, concurrency, session types
Liberating Merges via Apartness and Guarded Subtyping¶
Authors: Han Xu, Xuejing Huang, Bruno C. d. S. Oliveira
Venue: OOPSLA 2025
Year: 2025
This paper introduces apartness and guarded subtyping to enable disjoint merges in type systems with intersection types. The approach liberates the merge operator from overly restrictive disjointness conditions while maintaining coherence.
Keywords: intersection types, merge operator, subtyping, type systems, coherence
The Simple Essence of Monomorphization¶
Authors: Matthew Lutze, Philipp Schuster, Jonathan Immanuel Brachthäuser
Venue: OOPSLA 2025
Year: 2025
This paper presents a clean formal account of monomorphization for polymorphic type systems, showing how to systematically specialize polymorphic code to concrete types. The approach handles effects and other advanced type features.
Keywords: monomorphization, polymorphism, type systems, compilation
What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures¶
Authors: Yichen Xu, Oliver Bračevac, Nguyen Pham, Martin Odersky
Venue: OOPSLA 2025
Year: 2025
This paper extends capture tracking (as in Scala's Capture Calculus) to generic data structures, enabling ergonomic and expressive tracking of captured capabilities through type parameters. The approach avoids annotation burden while maintaining safety.
Keywords: capture tracking, effects, type systems, Scala, capabilities
Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation¶
Authors: Philipp Schuster, Marius Müller, Klaus Ostermann, Jonathan Immanuel Brachthäuser
Venue: OOPSLA 2025
Year: 2025
This paper shows that compiling the classical sequent calculus reveals a duality between evaluation order and calling conventions, providing a principled foundation for compiler design. The work bridges proof theory and compilation.
Keywords: sequent calculus, compilation, duality, calling conventions, proof theory
Tracing Just-in-time Compilation for Effects and Handlers¶
Authors: Marcial Gaißert, CF Bolz-Tereick, Jonathan Immanuel Brachthäuser
Venue: OOPSLA 2025
Year: 2025
This paper develops tracing JIT compilation for languages with algebraic effects and handlers, addressing the performance challenge of effect handler dispatch. The trace-based approach specializes handler code to specific effect use patterns.
Keywords: JIT compilation, algebraic effects, effect handlers, performance
Automated Discovery of Tactic Libraries for Interactive Theorem Proving¶
Authors: Yutong Xin, Jimmy Xin, Gabriel Poesia, Noah D. Goodman, Jocelyn Qiaochu Chen, Işıl Dillig
Venue: OOPSLA 2025
Year: 2025
This paper presents an automated method for discovering useful tactic libraries for interactive theorem provers from a corpus of proofs. The approach learns reusable proof patterns that reduce proof effort for new theorems.
Keywords: theorem proving, tactic synthesis, proof automation, machine learning
Incremental Bidirectional Typing via Order Maintenance¶
Authors: Thomas J. Porter, Marisa Kirisame, Ivan Wei, Pavel Panchekha, Cyrus Omar
Venue: OOPSLA 2025
Year: 2025
This paper presents an incremental bidirectional type-checking algorithm that efficiently updates type information as programs are edited, using order maintenance data structures to track dependencies. This enables responsive type checking in live programming environments.
Keywords: bidirectional typing, incremental computation, type checking, live programming