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

TPS: A Theorem-Proving System for Classical Type Theory. - Peter B. Andrews; Matthew Bishop; Sunil Issar; Dan Nesmith; Frank Pfenning; Hongwei Xi 001 (J. Autom. Reason., 1996)

Simulating eta-expansions with beta-reductions in the Second-Order Polymorphic lambda-calculus. - Hongwei Xi 001 (LFCS, 1997)

Evaluation Under Lambda Abstraction. - Hongwei Xi 001 (PLILP, 1997)

Weak and Strong Beta Normalisations in Typed Lambda-Calculi. - Hongwei Xi 001 (TLCA, 1997)

Eliminating Array Bound Checking Through Dependent Types. - Hongwei Xi 001; Frank Pfenning (PLDI, 1998)

Towards Automated Termination Proofs through "Freezing". - Hongwei Xi 001 (RTA, 1998)

Towards array bound check elimination in Java TM virtual machine language. - Hongwei Xi 001; Songtao Xia (CASCON, 1999)

Dead Code Elimination through Dependent Types. - Hongwei Xi 001 (PADL, 1999)

Dependent Types in Practical Programming. - Hongwei Xi 001; Frank Pfenning (POPL, 1999)

Perpetual Reductions in Lambda-Calculus. - Femke van Raamsdonk; Paula Severi; Morten Heine Sørensen; Hongwei Xi 001 (Inf. Comput., 1999)

Upper Bounds for Standardizations and An Application. - Hongwei Xi 001 (J. Symb. Log., 1999)

Imperative Programming with Dependent Types. - Hongwei Xi 001 (LICS, 2000)

A Dependently Typed Assembly Language. - Hongwei Xi 001; Robert Harper 001 (ICFP, 2001)

Unifying object-oriented programming with typed functional programming. - Hongwei Xi 001 (ASIA-PEPM, 2002)

Dependent Types for Program Termination Verification. - Hongwei Xi 001 (High. Order Symb. Comput., 2002)

A Typeful and Tagless Representation for XML Documents. - Dengping Zhu; Hongwei Xi 001 (APLAS, 2003)

Generating Heap-Bounded Programs in a Functional Setting. - Walid Taha; Stephan Ellner; Hongwei Xi 001 (EMSOFT, 2003)

Implementing typeful program transformations. - Chiyan Chen; Hongwei Xi 001 (PEPM, 2003)

Guarded recursive datatype constructors. - Hongwei Xi 001; Chiyan Chen; Gang Chen (POPL, 2003)

Facilitating Program Verification with Dependent Types. - Hongwei Xi 001 (SEFM, 2003)

Applied Type System: Extended Abstract. - Hongwei Xi 001 (TYPES, 2003)

A Typeful Approach to Object-Oriented Programming with Multiple Inheritance. - Chiyan Chen; Rui Shi; Hongwei Xi 001 (PADL, 2004)

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

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

ATS: A Language That Combines Programming with Theorem Proving. - Sa Cui; Kevin Donnelly; Hongwei Xi 001 (FroCoS, 2005)

Combining programming with theorem proving. - Chiyan Chen; Hongwei Xi 001 (ICFP, 2005)

Combining higher-order abstract syntax with first-order abstract syntax in ATS. - Kevin Donnelly; Hongwei Xi 001 (MERLIN, 2005)

Safe Programming with Pointers Through Stateful Views. - Dengping Zhu; Hongwei Xi 001 (PADL, 2005)

Development Separation in Lambda-Calculus. - Hongwei Xi 001 (WoLLIC, 2005)

Meta-programming through typeful code representation. - Chiyan Chen; Hongwei Xi 001 (J. Funct. Program., 2005)

Distributed meta-programming. - Rui Shi; Chiyan Chen; Hongwei Xi 001 (GPCE, 2006)

A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F. - Kevin Donnelly; Hongwei Xi 001 (LFMTP@FLoC, 2006)

Preface. - Aaron Stump; Hongwei Xi 001 (PLPV@IJCAR, 2006)

Implementing Typeful Program Transformations. - Chiyan Chen; Rui Shi; Hongwei Xi 001 (Fundam. Informaticae, 2006)

Attributive Types for Proof Erasure. - Hongwei Xi 001 (TYPES, 2007)

Dependent ML An approach to practical programming with dependent types. - Hongwei Xi 001 (J. Funct. Program., 2007)

A Simple and General Theoretical Account for Abstract Types. - Hongwei Xi 001 (SBMF, 2009)

Operating system development with ATS: work in progress: (abstract only). - Matthew Danish; Hongwei Xi 001 (ACM SIGPLAN Notices, 2009)

A Modality for Safe Resource Sharing and Code Reentrancy. - Rui Shi; Dengping Zhu; Hongwei Xi 001 (ICTAC, 2010)

Operating system development with ATS: work in progress. - Matthew Danish; Hongwei Xi 001 (PLPV, 2010)

A Programmer-Centric Approach to Program Verification in ATS - Zhiqiang Ren; Hongwei Xi 001 (CoRR, 2012)

A linear type system for multicore programming in ATS. - Rui Shi; Hongwei Xi 001 (Sci. Comput. Program., 2013)

Applying language-based static verification in an ARM operating system. - Matthew Danish; Hongwei Xi 001; Richard West (SIGBED Rev., 2013)

Using Lightweight Theorem Proving in an Asynchronous Systems Context. - Matthew Danish; Hongwei Xi 001 (NASA Formal Methods, 2014)

Formal Semantics of Runtime Monitoring, Verification, Enforcement and Control. - Zhe Chen 011; Ou Wei; Zhiqiu Huang; Hongwei Xi 001 (TASE, 2015)

A robust and efficient method for estimating enzyme complex abundance and metabolic flux from expression data. - Brandon E. Barker; Narayanan Sadagopan; Yiping Wang; Kieran Smallbone; Christopher R. Myers; Hongwei Xi 001; Jason W. Locasale; Zhenglong Gu (Comput. Biol. Chem., 2015)

Dependent Types for Multi-Rate Flows in Synchronous Programming. - William Blair; Hongwei Xi 001 (ML Family/OCaml, 2015)

Combining type-checking with model-checking for system verification. - Zhiqiang Ren; Hongwei Xi 001 (MEMOCODE, 2016)

Parametric Runtime Verification of C Programs. - Zhe Chen 011; Zhemin Wang; Yunlong Zhu; Hongwei Xi 001; Zhibin Yang (TACAS, 2016)

Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus. - Hongwei Xi 001; Zhiqiang Ren; Hanwen Wu; William Blair (CoRR, 2016)

Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions. - Hongwei Xi 001; Hanwen Wu (CoRR, 2016)

Propositions in Linear Multirole Logic as Multiparty Session Types. - Hongwei Xi 001; Hanwen Wu (CoRR, 2016)

Dependent Session Types. - Hanwen Wu; Hongwei Xi 001 (CoRR, 2017)

Applied Type System: An Approach to Practical Programming with Theorem-Proving. - Hongwei Xi 001 (CoRR, 2017)

Multirole Logic (Extended Abstract). - Hongwei Xi 001; Hanwen Wu (CoRR, 2017)

Multiparty Dependent Session Types (Extended Abstract). - Hanwen Wu; Hongwei Xi 001 (CoRR, 2018)

Implementing Linking in Multiparty Sessions (Extended Abstract). - Hanwen Wu; Hongwei Xi 001 (CoRR, 2018)

To Memory Safety through Proofs. - Hongwei Xi 001; Dengping Zhu (CoRR, 2018)

Many-target, Many-sensor Ship Tracking and Classification. - Leonard Kosta; John Irvine 001; Laura Seaman; Hongwei Xi 001 (HPEC, 2019)

Program Synthesis and Vulnerability Injection Using a Grammar VAE. - Leonard Kosta; Laura Seaman; Hongwei Xi 001 (J. Softw., 2019)

A Calculus of Inductive Linear Constructions. - Qiancheng Fu; Hongwei Xi 001 (TyDe@ICFP, 2023)

A Dependently Typed Language with Dynamic Equality. - Mark Lemay; Qiancheng Fu; William Blair; Cheng Zhang; Hongwei Xi 001 (TyDe@ICFP, 2023)

Multirole Logic and Multiparty Channels. - Hongwei Xi 001; Hanwen Wu (CoRR, 2023)

A Two-Level Linear Dependent Type Theory. - Qiancheng Fu; Hongwei Xi 001 (CoRR, 2023)