Aosen Xiong

Research

I care about static guarantees that survive contact with real codebases: precise enough to prove useful properties, and practical enough to fit into the way developers already write, review, and debug programs.

PICO / Java immutability
  • Designing a Java pluggable type system for transitive abstract immutability with readonly references.
  • Supporting class mutability polymorphism so existing class hierarchies can express mutable and immutable uses without duplicate variants.
  • Formalizing the type system in Rocq and proving type soundness plus immutability properties.
  • Evaluated PICO on Java Collections Framework code in OpenJDK 17 and other benchmarks, covering approximately 26,000 non-comment lines of Java code.
  • Supported by the 2023 Amazon Research Award Optional Type Systems for Model-Implementation Consistency.
Paper

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

GAIT / Generic Abstract Immutability Types
  • A mechanized study of generic types and abstract immutability.
  • Models the interaction between generics, immutability qualifiers, receiver-dependent mutability, qualifier polymorphism, and requalified type variables.
  • Proves core metatheory for a generic immutability calculus in Lean 4.
  • Built as an instance of the reusable qualifier framework.
Paper

Aosen Xiong and Werner Dietl. Generic Abstract Immutability Types. Accepted at IWACO 2026.
IWACO · publications

Reusable Qualifier Framework in Lean 4
  • A Lean 4 framework for mechanizing qualifier-based type systems.
  • Factors reusable infrastructure for qualifier lattices, static typing, runtime semantics, runtime typing, progress, preservation, and soundness packaging.
  • Includes multiple checker instances, including Nullness, Readonly, Tainting, Confidentiality, Universe, and PICO.
Status

Manuscript and artifact in preparation.

Semantic Immutability / racy derived caches
  • Studies when mutable derived caches inside immutable objects preserve semantic immutability.
  • Uses per-field write histories, cache protocols, and trace-robust method conditions to separate harmless lazy caching from unsafe races.
  • Proves a Rocq theorem connecting stable abstraction, valid histories, whole-value observations, and trace-robust methods to pure-result refinement.
  • Connects PICO's stable abstract-state guarantee to an Iris-style semantic model with weak field histories.
Status

Manuscript in preparation.