default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDHongwei Xi 0001
Person information
- affiliation: Boston University, MA, USA
- affiliation (former): University of Cincinnati, OH, USA
- affiliation (former): Oregon Graduate Institute, Department of Computer Science and Engineering, Portland, OR, USA
- affiliation (former): Carnegie Mellon University, Department of Mathematical Sciences, Pittsburgh, PA, USA
Other persons with the same name
- Hongwei Xi 0002 — Southeast University, School of Mechanical Engineering, Nanjing, China
- Hongwei Xi 0003
![[0000-0002-2885-8506]](https://dblp.dagstuhl.de/img/orcid-mark.12x12.png "0000-0002-2885-8506")
— Beijing University of Technology, Faculty of Information Technology, China
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2023
[c43]Qiancheng Fu, Hongwei Xi:
A Calculus of Inductive Linear Constructions. TyDe@ICFP 2023: 1-13- [c42]Mark Lemay, Qiancheng Fu, William Blair, Cheng Zhang, Hongwei Xi:
A Dependently Typed Language with Dynamic Equality. TyDe@ICFP 2023: 44-57 - [i12]Hongwei Xi, Hanwen Wu:
Multirole Logic and Multiparty Channels. CoRR abs/2309.01317 (2023) - [i11]Qiancheng Fu, Hongwei Xi:
A Two-Level Linear Dependent Type Theory. CoRR abs/2309.08673 (2023)
2010 – 2019
- 2019
- [j13]Leonard Kosta, Laura Seaman, Hongwei Xi:
Program Synthesis and Vulnerability Injection Using a Grammar VAE. J. Softw. 14(6): 227-246 (2019) - [c41]Leonard Kosta, John Irvine, Laura Seaman, Hongwei Xi:
Many-target, Many-sensor Ship Tracking and Classification. HPEC 2019: 1-7 - 2018
- [i10]Hanwen Wu, Hongwei Xi:
Multiparty Dependent Session Types (Extended Abstract). CoRR abs/1808.00077 (2018) - [i9]Hanwen Wu, Hongwei Xi:
Implementing Linking in Multiparty Sessions (Extended Abstract). CoRR abs/1810.12146 (2018) - [i8]Hongwei Xi, Dengping Zhu:
To Memory Safety through Proofs. CoRR abs/1810.12190 (2018) - 2017
- [i7]Hongwei Xi, Hanwen Wu:
Multirole Logic (Extended Abstract). CoRR abs/1703.06391 (2017) - [i6]Hongwei Xi:
Applied Type System: An Approach to Practical Programming with Theorem-Proving. CoRR abs/1703.08683 (2017) - [i5]Hanwen Wu, Hongwei Xi:
Dependent Session Types. CoRR abs/1704.07004 (2017) - 2016
- [c40]Zhiqiang Ren, Hongwei Xi:
Combining type-checking with model-checking for system verification. MEMOCODE 2016: 54-58 - [c39]Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi, Zhibin Yang:
Parametric Runtime Verification of C Programs. TACAS 2016: 299-315 - [i4]Hongwei Xi, Zhiqiang Ren, Hanwen Wu, William Blair:
Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus. CoRR abs/1603.03727 (2016) - [i3]Hongwei Xi, Hanwen Wu:
Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions. CoRR abs/1604.03020 (2016) - [i2]Hongwei Xi, Hanwen Wu:
Propositions in Linear Multirole Logic as Multiparty Session Types. CoRR abs/1611.08888 (2016) - 2015
- [j12]Brandon E. Barker, Narayanan Sadagopan, Yiping Wang, Kieran Smallbone, Christopher R. Myers, Hongwei Xi, Jason W. Locasale, Zhenglong Gu:
A robust and efficient method for estimating enzyme complex abundance and metabolic flux from expression data. Comput. Biol. Chem. 59: 98-112 (2015) - [c38]Zhe Chen, Ou Wei, Zhiqiu Huang, Hongwei Xi:
Formal Semantics of Runtime Monitoring, Verification, Enforcement and Control. TASE 2015: 63-70 - [c37]William Blair, Hongwei Xi:
Dependent Types for Multi-Rate Flows in Synchronous Programming. ML Family/OCaml 2015: 36-44 - 2014
- [c36]Matthew Danish, Hongwei Xi:
Using Lightweight Theorem Proving in an Asynchronous Systems Context. NASA Formal Methods 2014: 158-172 - 2013
- [j11]Rui Shi, Hongwei Xi:
A linear type system for multicore programming in ATS. Sci. Comput. Program. 78(8): 1176-1192 (2013) - [j10]Matthew Danish, Hongwei Xi, Richard West:
Applying language-based static verification in an ARM operating system. SIGBED Rev. 10(2): 16 (2013) - 2012
- [i1]Zhiqiang Ren, Hongwei Xi:
A Programmer-Centric Approach to Program Verification in ATS. CoRR abs/1203.6102 (2012) - 2010
- [c35]Rui Shi, Dengping Zhu, Hongwei Xi:
A Modality for Safe Resource Sharing and Code Reentrancy. ICTAC 2010: 382-396 - [c34]Matthew Danish, Hongwei Xi:
Operating system development with ATS: work in progress. PLPV 2010: 9-14
2000 – 2009
- 2009
- [j9]Matthew Danish, Hongwei Xi:
Operating system development with ATS: work in progress: (abstract only). ACM SIGPLAN Notices 44(11): 6 (2009) - [c33]Hongwei Xi:
A Simple and General Theoretical Account for Abstract Types. SBMF 2009: 336-349 - 2007
- [j8]Hongwei Xi:
Dependent ML An approach to practical programming with dependent types. J. Funct. Program. 17(2): 215-286 (2007) - [c32]Hongwei Xi:
Attributive Types for Proof Erasure. TYPES 2007: 188-202 - [e2]Aaron Stump, Hongwei Xi:
Proceedings of the Programming Languages meets Program Verification, PLPV@IJCAR 2006, Part of FLoC 2006, Seattle, WA, USA, August 21, 2006. Electronic Notes in Theoretical Computer Science 174(7), Elsevier 2007 [contents] - [e1]Aaron Stump, Hongwei Xi:
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 [contents] - 2006
- [j7]Chiyan Chen, Rui Shi, Hongwei Xi:
Implementing Typeful Program Transformations. Fundam. Informaticae 69(1-2): 103-121 (2006) - [c31]Rui Shi, Chiyan Chen, Hongwei Xi:
Distributed meta-programming. GPCE 2006: 243-248 - [c30]Aaron Stump, Hongwei Xi:
Preface. PLPV@IJCAR 2006: 1-2 - [c29]Kevin Donnelly, Hongwei Xi:
A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F. LFMTP@FLoC 2006: 109-125 - 2005
- [j6]Chiyan Chen, Hongwei Xi:
Meta-programming through typeful code representation. J. Funct. Program. 15(5): 797-835 (2005) - [c28]Sa Cui, Kevin Donnelly, Hongwei Xi:
ATS: A Language That Combines Programming with Theorem Proving. FroCoS 2005: 310-320 - [c27]Kevin Donnelly, Hongwei Xi:
Combining higher-order abstract syntax with first-order abstract syntax in ATS. MERLIN 2005: 58-63 - [c26]Chiyan Chen, Hongwei Xi:
Combining programming with theorem proving. ICFP 2005: 66-77 - [c25]Dengping Zhu, Hongwei Xi:
Safe Programming with Pointers Through Stateful Views. PADL 2005: 83-97 - [c24]Hongwei Xi:
Development Separation in Lambda-Calculus. WoLLIC 2005: 207-221 - 2004
- [j5]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. Reason. 32(1): 75-92 (2004) - [c23]Chiyan Chen, Rui Shi, Hongwei Xi:
A Typeful Approach to Object-Oriented Programming with Multiple Inheritance. PADL 2004: 23-38 - [c22]Chiyan Chen, Dengping Zhu, Hongwei Xi:
Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell. PADL 2004: 239-254 - 2003
- [c21]Dengping Zhu, Hongwei Xi:
A Typeful and Tagless Representation for XML Documents. APLAS 2003: 89-104 - [c20]Walid Taha, Stephan Ellner, Hongwei Xi:
Generating Heap-Bounded Programs in a Functional Setting. EMSOFT 2003: 340-355 - [c19]Chiyan Chen, Hongwei Xi:
Meta-programming through typeful code representation. ICFP 2003: 275-286 - [c18]Chiyan Chen, Hongwei Xi:
Implementing typeful program transformations. PEPM 2003: 20-28 - [c17]Hongwei Xi, Chiyan Chen, Gang Chen:
Guarded recursive datatype constructors. POPL 2003: 224-235 - [c16]Hongwei Xi:
Facilitating Program Verification with Dependent Types. SEFM 2003: 72-81 - [c15]Hongwei Xi:
Applied Type System: Extended Abstract. TYPES 2003: 394-408 - 2002
- [j4]Hongwei Xi:
Dependent Types for Program Termination Verification. High. Order Symb. Comput. 15(1): 91-131 (2002) - [c14]Hongwei Xi:
Unifying object-oriented programming with typed functional programming. ASIA-PEPM 2002: 117-125 - 2001
- [c13]Hongwei Xi, Robert Harper:
A Dependently Typed Assembly Language. ICFP 2001: 169-180 - [c12]Hongwei Xi:
Dependent Types for Program Termination Verification. LICS 2001: 231-242 - 2000
- [c11]Hongwei Xi:
Imperative Programming with Dependent Types. LICS 2000: 375-387
1990 – 1999
- 1999
- [j3]Femke van Raamsdonk, Paula Severi, Morten Heine Sørensen, Hongwei Xi:
Perpetual Reductions in Lambda-Calculus. Inf. Comput. 149(2): 173-225 (1999) - [j2]Hongwei Xi:
Upper Bounds for Standardizations and An Application. J. Symb. Log. 64(1): 291-303 (1999) - [c10]Hongwei Xi, Songtao Xia:
Towards array bound check elimination in Java TM virtual machine language. CASCON 1999: 14 - [c9]Hongwei Xi:
Dead Code Elimination through Dependent Types. PADL 1999: 228-242 - [c8]Hongwei Xi, Frank Pfenning:
Dependent Types in Practical Programming. POPL 1999: 214-227 - 1998
- [c7]Hongwei Xi, Frank Pfenning:
Eliminating Array Bound Checking Through Dependent Types. PLDI 1998: 249-257 - [c6]Hongwei Xi:
Towards Automated Termination Proofs through "Freezing". RTA 1998: 271-285 - 1997
- [c5]Hongwei Xi:
Upper Bounds for Standardizations and an Application. Kurt Gödel Colloquium 1997: 335-348 - [c4]Hongwei Xi:
Simulating eta-expansions with beta-reductions in the Second-Order Polymorphic lambda-calculus. LFCS 1997: 399-409 - [c3]Hongwei Xi:
Evaluation Under Lambda Abstraction. PLILP 1997: 259-273 - [c2]Hongwei Xi:
Weak and Strong Beta Normalisations in Typed Lambda-Calculi. TLCA 1997: 390-404 - 1996
- [j1]Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi:
TPS: A Theorem-Proving System for Classical Type Theory. J. Autom. Reason. 16(3): 321-353 (1996) - 1993
- [c1]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
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-09-16 00:52 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
