Demo Data from SIGIR 2026 / reviewers in the wild / expert
Cao Nguyen Pham
dblp:400/8095
· DBLP profile ↗
1ranked-venue papers
0as first author
1since 2021 · last 2025
0009-0005-2543-3309ORCID · reported
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 1 · 1 since 2021
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Software engineering, system software, and programming languages
1 paper |
Programming languages and type systems · 70% Program verification · 30% |
Topics — the 3 heaviest of 4, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Programming languages and type systems › computational effects
effect systems |
0.9 | 1 | 2025 | What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures · Proc. ACM Program. Lang. 2025 |
Program verification › mechanized verification
mechanized metatheory |
0.9 | 1 | 2025 | What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures · Proc. ACM Program. Lang. 2025 |
Programming languages and type systems › type systems
type soundness |
0.9 | 1 | 2025 | What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures · Proc. ACM Program. Lang. 2025 |
Methods — techniques the papers use, named apart from their topics
type-preserving translation · 0.9reach capabilities · 0.9existential capture set quantification · 0.9
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data StructuresabstractCapturing types in Scala unify static effect and resource tracking with object capabilities, enabling lightweight effect polymorphism with minimal notational overhead. However, their expressiveness has been insufficient for tracking capabilities embedded in generic data structures, preventing them from scaling to the standard collections library - an essential prerequisite for broader adoption. This limitation stems from the inability to name capabilities within the system's notion of box types. This paper develops System Capless, a new foundation for capturing types that provides the theoretical basis for reach capabilities (rcaps), a novel mechanism for naming "what's in the box". The calculus refines the universal capability notion into a new scheme with existential and universal capture set quantification. Intuitively, rcaps witness existentially quantified capture sets inside the boxes of generic types in a way that does not require exposing existential capture types in the surface language. We have fully mechanized the formal metatheory of System Capless in Lean, including proofs of type soundness and scope safety. System Capless supports the same lightweight notation of capturing types plus rcaps, as certified by a type-preserving translation, and also enables fully optional explicit capture-set quantification to increase expressiveness. Finally, we present a full reimplementation of capture checking in Scala 3 based on System Capless and migrate the entire Scala collections library and an asynchronous programming library to evaluate its practicality and ergonomics. Our results demonstrate that reach capabilities enable the adoption of capture checking in production code with minimal changes and minimal-to-zero notational overhead in a vast majority of cases. Yichen Xu 0008, Oliver Bracevac, Cao Nguyen Pham, Martin Odersky |
Proc. ACM Program. Lang. | 3 |