| 2023 | ICFP | A Calculus of Inductive Linear Constructions. | Qiancheng Fu, Hongwei Xi |
| 2023 | ICFP | A Dependently Typed Language with Dynamic Equality. | Mark Lemay, Qiancheng Fu, William Blair, Cheng Zhang, Hongwei Xi |
| 2016 | HCI | Study on the Target Frame of HMDs in Different Background Brightness. | Jiang Shao, Haiyan Wang, Rui Zhao, Jing Zhang, Zhangfan Shen, Hongwei Xi |
| 2016 | MEMOCODE | Combining type-checking with model-checking for system verification. | Zhiqiang Ren, Hongwei Xi |
| 2016 | TACAS | Parametric Runtime Verification of C Programs. | Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi, Zhibin Yang |
| 2015 | TASE | Formal Semantics of Runtime Monitoring, Verification, Enforcement and Control. | Zhe Chen, Ou Wei, Zhiqiu Huang, Hongwei Xi |
| 2010 | ICTAC | A Modality for Safe Resource Sharing and Code Reentrancy. | Rui Shi, Dengping Zhu, Hongwei Xi |
| 2006 | GPCE | Distributed meta-programming. | Rui Shi, Chiyan Chen, Hongwei Xi |
| 2005 | ICFP | Combining programming with theorem proving. | Chiyan Chen, Hongwei Xi |
| 2005 | ICFP | Combining higher-order abstract syntax with first-order abstract syntax in ATS. | Kevin Donnelly, Hongwei Xi |
| 2005 | PADL | Safe Programming with Pointers Through Stateful Views. | Dengping Zhu, Hongwei Xi |
| 2004 | PADL | A Typeful Approach to Object-Oriented Programming with Multiple Inheritance. | Chiyan Chen, Rui Shi, Hongwei Xi |
| 2004 | PADL | Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell. | Chiyan Chen, Dengping Zhu, Hongwei Xi |
| 2003 | APLAS | A Typeful and Tagless Representation for XML Documents. | Dengping Zhu, Hongwei Xi |
| 2003 | EMSOFT | Generating Heap-Bounded Programs in a Functional Setting. | Walid Taha, Stephan Ellner, Hongwei Xi |
| 2003 | ICFP | Meta-programming through typeful code representation. | Chiyan Chen, Hongwei Xi |
| 2003 | PEPM | Implementing typeful program transformations. | Chiyan Chen, Hongwei Xi |
| 2003 | POPL | Guarded recursive datatype constructors. | Hongwei Xi, Chiyan Chen, Gang Chen |
| 2003 | SEFM | Facilitating Program Verification with Dependent Types. | Hongwei Xi |
| 2002 | PEPM | Unifying object-oriented programming with typed functional programming. | Hongwei Xi |
| 2001 | ICFP | A Dependently Typed Assembly Language. | Hongwei Xi, Robert Harper |
| 2001 | LICS | Dependent Types for Program Termination Verification. | Hongwei Xi |
| 2000 | LICS | Imperative Programming with Dependent Types. | Hongwei Xi |
| 1999 | PADL | Dead Code Elimination through Dependent Types. | Hongwei Xi |
| 1999 | POPL | Dependent Types in Practical Programming. | Hongwei Xi, Frank Pfenning |
| 1998 | PLDI | Eliminating Array Bound Checking Through Dependent Types. | Hongwei Xi, Frank Pfenning |
| 1997 | LFCS | Simulating eta-expansions with beta-reductions in the Second-Order Polymorphic lambda-calculus. | Hongwei Xi |