Hongwei Xi

Zhiqiang Ren, Hongwei Xi: A Programmer-Centric Approach to Program Verification in ATS. CoRR abs/1203.6102 (2012)

Rui Shi, Dengping Zhu, Hongwei Xi: A Modality for Safe Resource Sharing and Code Reentrancy. ICTAC 2010: 382-396

Matthew Danish, Hongwei Xi: Operating system development with ATS: work in progress. PLPV 2010: 9-14

Matthew Danish, Hongwei Xi: Operating system development with ATS: work in progress: (abstract only). SIGPLAN Notices 44(11): 6 (2009)

Hongwei Xi: A Simple and General Theoretical Account for Abstract Types. SBMF 2009: 336-349

Kevin Donnelly, Hongwei Xi: A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F. Electr. Notes Theor. Comput. Sci. 174(5): 109-125 (2007)

Aaron Stump, Hongwei Xi: Preface. Electr. Notes Theor. Comput. Sci. 174(7): 1-2 (2007)

Hongwei Xi: Dependent ML An approach to practical programming with dependent types. J. Funct. Program. 17(2): 215-286 (2007)

Hongwei Xi: Attributive Types for Proof Erasure. TYPES 2007: 188-202

Aaron Stump, Hongwei Xi (Eds.): Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007. ACM 2007, isbn 978-1-59593-677-6

Hongwei Xi: Development Separation in Lambda-Calculus. Electr. Notes Theor. Comput. Sci. 143: 207-221 (2006)

Chiyan Chen, Rui Shi, Hongwei Xi: Implementing Typeful Program Transformations. Fundam. Inform. 69(1-2): 103-121 (2006)

Rui Shi, Chiyan Chen, Hongwei Xi: Distributed meta-programming. GPCE 2006: 243-248

Chiyan Chen, Hongwei Xi: Meta-programming through typeful code representation. J. Funct. Program. 15(5): 797-835 (2005)

Sa Cui, Kevin Donnelly, Hongwei Xi: ATS: A Language That Combines Programming with Theorem Proving. FroCoS 2005: 310-320

Kevin Donnelly, Hongwei Xi: Combining higher-order abstract syntax with first-order abstract syntax in ATS. MERLIN 2005: 58-63

Chiyan Chen, Hongwei Xi: Combining programming with theorem proving. ICFP 2005: 66-77

Dengping Zhu, Hongwei Xi: Safe Programming with Pointers Through Stateful Views. PADL 2005: 83-97

Peter B. Andrews, Chad E. Brown, Frank Pfenning, Matthew Bishop, Sunil Issar, Hongwei Xi: ETPS: A System to Help Students Write Formal Proofs. J. Autom. Reasoning 32(1): 75-92 (2004)

Chiyan Chen, Rui Shi, Hongwei Xi: A Typeful Approach to Object-Oriented Programming with Multiple Inheritance. PADL 2004: 23-38

Chiyan Chen, Dengping Zhu, Hongwei Xi: Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell. PADL 2004: 239-254

Chiyan Chen, Hongwei Xi: Meta-programming through typeful code representation. SIGPLAN Notices 38(9): 275-286 (2003)

Dengping Zhu, Hongwei Xi: A Typeful and Tagless Representation for XML Documents. APLAS 2003: 89-104

Walid Taha, Stephan Ellner, Hongwei Xi: Generating Heap-Bounded Programs in a Functional Setting. EMSOFT 2003: 340-355

Chiyan Chen, Hongwei Xi: Meta-programming through typeful code representation. ICFP 2003: 275-286

Chiyan Chen, Hongwei Xi: Implementing typeful program transformations. PEPM 2003: 20-28

Hongwei Xi, Chiyan Chen, Gang Chen: Guarded recursive datatype constructors. POPL 2003: 224-235

Hongwei Xi: Facilitating Program Verification with Dependent Types. SEFM 2003: 72-81

Hongwei Xi: Applied Type System: Extended Abstract. TYPES 2003: 394-408

Hongwei Xi: Dependent Types for Program Termination Verification. Higher-Order and Symbolic Computation 15(1): 91-131 (2002)

Hongwei Xi: Unifying object-oriented programming with typed functional programming. ASIA-PEPM 2002: 117-125

Hongwei Xi, Robert Harper: A Dependently Typed Assembly Language. ICFP 2001: 169-180

Hongwei Xi: Dependent Types for Program Termination Verification. LICS 2001: 231-242

Hongwei Xi: Imperative Programming with Dependent Types. LICS 2000: 375-387

Femke van Raamsdonk, Paula Severi, Morten Heine Sørensen, Hongwei Xi: Perpetual Reductions in Lambda-Calculus. Inf. Comput. 149(2): 173-225 (1999)

Hongwei Xi: Upper Bounds for Standardizations and An Application. J. Symb. Log. 64(1): 291-303 (1999)

Hongwei Xi, Songtao Xia: Towards array bound check elimination in Java ^TM virtual machine language. CASCON 1999: 14

Hongwei Xi: Dead Code Elimination through Dependent Types. PADL 1999: 228-242

Hongwei Xi, Frank Pfenning: Dependent Types in Practical Programming. POPL 1999: 214-227

Hongwei Xi, Frank Pfenning: Eliminating Array Bound Checking Through Dependent Types. PLDI 1998: 249-257

Hongwei Xi: Towards Automated Termination Proofs through "Freezing". RTA 1998: 271-285

Hongwei Xi: Upper Bounds for Standardizations and an Application. Kurt Gödel Colloquium 1997: 335-348

Hongwei Xi: Simulating eta-expansions with beta-reductions in the Second-Order Polymorphic lambda-calculus. LFCS 1997: 399-409

Hongwei Xi: Evaluation Under Lambda Abstraction. PLILP 1997: 259-273

Hongwei Xi: Weak and Strong Beta Normalisations in Typed Lambda-Calculi. TLCA 1997: 390-404

Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi: TPS: A Theorem-Proving System for Classical Type Theory. J. Autom. Reasoning 16(3): 321-353 (1996)

Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi: TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory. HUG 1993: 366-370