Publications

• Typestate via Revocable Capabilities.
  Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, Tiark Rompf.
  [PLDI26]

• Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types.
  Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, Tiark Rompf.
  [PLDI26]

• When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking.
  Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf.
  [OOPSLA26]

• Complete the Cycle: Reachability Types with Expressive Cyclic References.
  Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf.
  [OOPSLA25]

• Modeling Reachability Types with Logical Relations: Semantic Type Soundness, Termination, Effect Safety, and Equational Theory.
  Yuyan Bao, Songlin Jia, Guannan Wei, Oliver Bračevac, Tiark Rompf.
  [OOPSLA25]

• Polymorphic reachability types: Tracking freshness, aliasing, and separation in higher-order generic programs.
  Guannan Wei, Oliver Bračevac, Songlin Jia, Yuyan Bao, Tiark Rompf.
  [POPL24]

• Graph IRs for Impure Higher-Order Languages – Making Aggressive Optimizations Affordable with Precise Effect Dependencies.
  Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe , Yuxuan Jiang, Yuyan Bao, Tiark Rompf.
  [OOPSLA23]

• Cache Refinement Type for Side-channel Detection of Cryptographic Software.
  Ke Jiang, Yuyan Bao, Shuai Wang, Zhibo Liu, Tianwei Zhang.
  [CCS22]

• SoK: Demystifying Binary Lifters Through the Lens of Downstream Applications.
  Zhibo Liu, Yuanyuan Yuan, Shuai Wang, Yuyan Bao.
  [IEEE S&P22]

• Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs.
  Yuyan Bao, Guannan Wei, Oliver Bračevac, Yuxuan Jiang, Qiyang He, Tiark Rompf.
  [OOPSLA21]

• HACCLE: Metaprogramming for Secure Multi-Party Computation.
  Yuyan Bao, Kirshanthan Sundararajah, Raghav Malik, Qianchuan Ye, Christopher Wagner, Nouraldin Jaber, Fei Wang, Mohammad Hassan Ameri, Donghang Lu, Alexander Seto, Benjamin Delaware, Roopsha Samanta, Aniket Kate, Christina Garman, Jeremiah Blocki, Pierre-David Letourneau, Benoit Meister, Jonathan Springer, Tiark Rompf, Milind Kulkarni.
  [GPCE21]

• Verifying Verified Code.
  Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel.
  [ATVA21]

• Identifying Cache-Based Side Channels through Secret-Augmented Abstract Interpretation.
  Shuai Wang, Yuyan Bao, Xiao Liu, Pei Wang, Danfeng Zhang, Dinghao Wu.
  [USENIX Security19]

• A Methodology for Invariants, Framing, and Subtyping in JML.
  Yuyan Bao, Gary T. Leavens.
  [Book Chapter18]

• Unifying Separation Logic and Region Logic to Allow Interoperability.
  Yuyan Bao, Gary T. Leavens, Gidon Ernst.
  [FAC18]

• Conditional Effects in Fine-Grained Region Logic.
  Yuyan Bao, Gary T. Leavens, Gidon Ernst.
  [FTfJP15]