HKU PL Group Papers - Index

This folder is a fast-pass Obsidian/Quartz knowledge base generated from HKU PL Group papers related to iso-recursive subtyping, intersection/union types, disjointness, merges, and compositional programming.

Important: the Markdown notes are generated with pymupdf4llm; original PDFs are kept in _pdfs/, and extracted figures/images are kept in _assets/. For proof-critical use, verify exact inference rules, lemmas, and equations against the linked PDF.

Research map

• Iso-recursive subtyping: New designs for iso-recursive subtyping and their integration with language features.
• Intersection and union duality: Duality between intersection and union types, splits, and simplification of metatheories.
• Merge operator and disjointness: Merge operator, disjoint intersection types, disjoint polymorphism, nested composition, type difference, dependent merges, and type-directed operational semantics.
• Compositional programming: Compositional programming with merge calculi and first-class traits for modularity and extensibility.

Papers by area

Iso-recursive subtyping

• Recursive Subtyping for All — JFP — OK
• QuickSub Efficient Iso-Recursive Subtyping — POPL’25 — OK
• Full Iso-Recursive Types — OOPSLA’24 — OK
• A Calculus with Recursive Types, Record Concatenation and Subtyping — APLAS’22 — OK
• Revisiting Iso-Recursive Subtyping — TOPLAS — OK

Intersection and union duality

• Named Arguments as Intersections, Optional Arguments as Unions — ESOP’25 — OK
• Disjoint Polymorphism with Intersection and Union Types — FTfJP’24 — OK
• Union Types with Disjoint Switches — ECOOP’22 — OK
• Distributing Intersection and Union Types with Splits and Duality (Functional Pearl) — ICFP’21 — OK
• The Duality of Subtyping — ECOOP’20 — OK

Merge operator and disjointness

• Liberating Merges via Apartness and Guarded Subtyping — OOPSLA’25 — OK
• A Case for First-Class Environments — OOPSLA’24 — OK
• Dependent Merges and First-Class Environments — ECOOP’23 — OK
• A Bowtie for a Beast Overloading, Eta Expansion, and Extensible Data Types in Fbowtie — POPL’23 — OK
• Making a Type Difference Subtraction on Intersection Types as Generalized Record Operations — POPL’23 — OK
• Applicative Intersection Types — APLAS’22 — OK
• Direct Foundations for Compositional Programming — ECOOP’22 — OK
• Taming the Merge Operator — JFP — OK
• Row and Bounded Polymorphism via Disjoint Polymorphism — ECOOP’20 — OK
• Distributive Disjoint Polymorphism for Compositional Programming — ESOP’19 — OK
• The Essence of Nested Composition — ECOOP’18 — OK
• Disjoint Polymorphism — ESOP’17 — OK
• Disjoint Intersection Types — ICFP’16 — OK

Compositional programming

• Type-Safe Compilation of Dynamic Inheritance via Merging — TOPLAS — OK
• Imperative Compositional Programming — OOPSLA’24 — OK
• Compositional Embeddings of Domain-Specific Languages — OOPSLA’22 — OK
• Compositional Programming — TOPLAS — OK
• Shallow EDSLs and Object-Oriented Programming — ‘19 — OK
• Typed First-Class Traits — ECOOP’18 — OK

Suggested proof-agent reading order for iso-recursive subtyping

1. Revisiting Iso-Recursive Subtyping
2. Full Iso-Recursive Types
3. QuickSub Efficient Iso-Recursive Subtyping
4. Recursive Subtyping for All
5. A Calculus with Recursive Types, Record Concatenation and Subtyping
6. Distributing Intersection and Union Types with Splits and Duality (Functional Pearl)
7. The Duality of Subtyping
8. Disjoint Intersection Types
9. Disjoint Polymorphism

Files

• PDFs: _pdfs/
• Extracted assets: _assets/
• Metadata: papers.metadata.json