Accepted Paper

• When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking
  Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
  OOPSLA 26. Extended Version. pdf

• Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
  Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, Tiark Rompf
  PLDI 26. Extended Version. pdf

• Typestate via Revocable Capabilities
  Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Tiark Rompf
  PLDI 26. Arxiv Version. pdf

• Complete the Cycle: Reachability Types with Expressive Cyclic References
  Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
  OOPSLA 25. pdf

  
  

Submitted Paper

• Let Functions Speak: Lightweight Parametric Polymorphism via Domain and Range Types
  Siyuan He, Songlin Jia, Tiark Rompf
  Submitted to OOPSLA 26 R2. arxiv

• Free to Move: Reachability Types with Flow-Sensitive Effects for Safe Deallocation and Ownership Transfer
  Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf
  Submitted to OOPSLA 26 R2. arxiv

  
  

Early Paper

• Verification of an Airport Taxiway Path-Finding Algorithm
  Siyuan He, Ke Du, Joshua Wilhelm, Jean-Baptiste Jeannin
  DASC 2020. Best of Session. pdf

  
  

Other Documents

• Presentation: Verification of an Airport Taxiway Path-Finding Algorithm. DASC 2020. Slides