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 in automated reasoning.
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.
Rocq proof · publications

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. Submitted to IWACO 2026. See 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.