Publications

Papers and manuscripts. Mechanized artifacts are linked where they are public.

Accepted

1. Aosen Xiong, Yudi Bai, Haifeng Shi, Lian Sun, Mier Ta, and Werner Dietl. Transitive, Abstract, and Class Polymorphic Immutability. To appear at OOPSLA 2026. Rocq proof

Under Review

1. Aosen Xiong and Werner Dietl. Generic Abstract Immutability Types. Submitted to IWACO 2026.

In Preparation

• Reusable qualifier framework in Lean 4 — manuscript and artifact in preparation.
• Semantic immutability for racy derived caches — manuscript in preparation.

Project background and technical detail for each of these lines of work is on the research page.