
Hongwei Xi
Publications
Journals
 Rui Shi and
Hongwei Xi,
A
Linear Type System for Multicore Programming,
Science of Computer
Programming, 2012.
 Hongwei Xi, Dependent ML: an approach to practical programming
with dependent types, Journal of Functional Programming (JFP), vol. 17(2),
pp. 215286, 2007.
(bibtex)
(pdf)
(ps)
 Chiyan Chen,
Rui Shi and
Hongwei Xi, Implementing Typeful Program Transformations,
Fundamenta Informaticae, vol. 69 (12), pp. 103121,
2005.
(bibtex)
(pdf)
(ps)
 Chiyan Chen and
Hongwei Xi, MetaProgramming through Typeful Code Representation,
Journal of Functional Programming,
vol. 15(6), pp. 797835, 2005.
(bibtex)
(pdf)
(ps)
 Peter
B. Andrews, Matthew Bishop, Chad Brown, Sunil
Issar, Frank Pfenning
and Hongwei Xi, ETPS: A System to Help Students Write Formal Proofs,
Journal of Automated Reasoning (JAR), vol. 32(1), pp. 7592, 2004.
(pdf)
(ps)
 Hongwei Xi,
Dependently Typed Pattern Matching, Journal of Universal Computer Science
(JUCS), 9(8), pp. 851872, August 2003.
(bibtex)
(pdf) (ps)
 Hongwei Xi,
Dependent Types for Program Termination Verification,
Journal of HigherOrder Symbolic Computation, 15(1), pp. 91131, March 2002.
(bibtex)
(pdf)
(ps)
 Femke van Raamsdonk, Paula Severi, Morten H. Sorensen and Hongwei Xi,
Perpetual Reductions in LambdaCalculus,
Journal of Information and Computation, 149(2), pp. 173225, March 1999.
(bibtex)
(pdf)
(ps)
 Hongwei Xi, Upper bounds for standardisation and an application,
Journal of Symbolic Logic, 64(1), pp. 291303, March 1999.
(bibtex)
(pdf)
(ps)
 Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning,
and Hongwei Xi,
TPS: A Theorem Proving System for Classical Type Theory, Journal of Automated Reasoning, 16(3), pp. 321353, 1996.
(bibtex)
(pdf)
 Hongwei Xi, HalfClosed Intervals of Rescursively Enumerable Degrees
(in Chinese with English abstract),
Math. Semiannuals of Nanjing University, P.R. China, 1989.
Conferences and Symposiums

Matthew Danish
and Hongwei Xi, Using lightweight theorem proving in an
asynchronous systems context. In Proceedings of the Sixth NASA Formal
Methods Symposium. Houston, TX, April 30, 2014.
(pdf)

Rui Shi,
Dengping Zhu,
and Hongwei Xi,
A Modality for Safe Resource Sharing and Code Reentrancy.
In Proceedings of International Colloqium on Theoretical Aspects of Computing
(ICTAC'10), LNCS 6255, pp. 382396, Natal, Brazil, September 13, 2010.
(bibtex)
(pdf)
(ps)
(slides in ps)
(slides in pdf)
 Hongwei Xi, A Simple and General Theoretical Account for
Abstract Types. In the Proceedings of Brazilian Symposium on Formal
Methods (SBMF'09), LNCS 5902, pp. 336349, Gramado, Brazil, August 1921, 2009.
(bibtex)
(pdf)
(ps)
(slides in ps)
(slides in pdf)
 Rui Shi and
Hongwei Xi, A Linear Type System for Multicore Programming.
In Proceedings of Simposio Brasileiro de Linguagens de Programacao
(SBLP'09), Gramado, Brazil, August 1921, 2009.
(bibtex)
(pdf)
(ps)
(slides in ps)
(slides in pdf)

Rui Shi,
Chiyan Chen and
Hongwei Xi, Distributed MetaProgramming. In Proceedings of the 5th
International Conference on Generative Programming and Component
Engineering (GPCE'06), Portland, OR,
October 2006.
(bibtex)
(pdf)
(ps)
(slides in ppt)
 Chiyan Chen and
Hongwei Xi, Combining Programming with Theorem Proving. In
Proceedings of the 10th International Conference on Functional Programming
(ICFP'05), pp. 6677, Tallinn,
Estonia, September 2005.
(bibtex)
(pdf)
(ps)
(slides in pdf)
 Dengping Zhu and
Hongwei Xi, Safe Programming with Pointers through Stateful Views.
In Proceedings of the 7th International Symposium on Practical Aspects of
Declarative Languages (PADL'05), SpringerVerlag LNCS vol. 3350,
pp. 8397, Long Beach, CA, January 2005. (bibtex) (pdf)
(ps) (slides in
ppt)
 Chiyan Chen,
Rui Shi and
Hongwei Xi, A Typeful Approach to ObjectOriented Programming with
Multiple Inheritance. In Proceedings of the 6th International Symposium on
Practical Aspects of Declarative Languages (PADL'04), SpringerVerlag LNCS
vol. 3057, pp. 2338, Dallas, TX, June 2004. (bibtex) (pdf) (ps) (slides in ppt)
 Chiyan Chen,
Dengping Zhu and
Hongwei Xi, Implementing Cut Elimination: A Case Study of Simulating
Dependent Types in Haskell. In Proceedings of the 6th International
Symposium on Practical Aspects of Declarative Languages (PADL'04),
SpringerVerlage LNCS vol. 3057, pp. 239254, Dallas, TX, June 2004. (bibtex) (pdf) (ps) (slides in ppt)
 Dengping Zhu and Hongwei
Xi, A Typeful and Tagless Representation for XML Documents. In
Proceedings of the First Asian Symposium on Programming Languages and
Systems (APLAS'03),
SpringerVerlag LNCS vol. 2895, pp. 89104, Beijing, China, November 2003.
(bibtex)
(pdf)
(ps)
 Walid Taha, Stephan Ellner and Hongwei Xi, Generating
Imperative, HeapBounded Programs in a Functional Setting. In Proceedings
of the Third International Conference on Embedded Software (EMSOFT'03),
SpringerVerlag LNCS vol. 2855, pp. 340355, Philadelphia, PA, October
2003.
(bibtex)
(pdf)
(ps)
 Hongwei Xi,
Facilitating Program Verification with Dependent Types.
In Proceedings of International Conference on Software Engineering and
Formal Methods (SEFM'03), pp. 7281,
Brisbane, Australia, September 2003.
(bibtex)
(pdf)
(ps)
(slides in ppt)
 Chiyan Chen and Hongwei Xi,
MetaProgramming through Typeful Code Representation.
In Proceedings of the 8th International Conference on Functional Programming
(ICFP'03),
pp. 275286, Uppsala, Sweden, August 2003.
(bibtex)
(pdf)
(ps)
(slides in ppt)
 Hongwei Xi, Dependently Typed Pattern Matching. In Proceedings
of Simposio Brasileiro de Linguagens de Programacao
(SBLP'03),
pp. 149165, Ouro Preto, Brazil, May 2003.
(bibtex)
(pdf)
(ps)
(slides in ppt)
 Hongwei Xi, Chiyan Chen and Gang Chen,
Guarded Recursive Datatype Constructors.
In Proceedings of the 30th ACM SIGPLAN Symposium on
Principles of Programming Languages
(POPL'03),
pp. 224235, New Orleans, Louisiana, January 2003.
(bibtex)
(pdf)
(ps)
(slides in ppt)
 Hongwei Xi and Robert Harper, Dependently Typed
Assembly Language. In Proceedings of the 6th International Conference on
Functional Programming (ICFP'01), pp. 169180, Florence, September 2001.
(bibtex)
(pdf)
(ps)
 Hongwei Xi, Dependent Types for Program Termination
Verification. In Proceedings of 16th Symposium on Logic in Computer Science
(LICS'01), pp. 231242, Boston, June 2001. (bibtex) (pdf)
(ps)
 Hongwei Xi, Imperative Programming with Dependent Types, In
Proceedings of 15th Symposium on Logic in Computer Science (LICS'00),
pp. 375387, Santa Barbara, June 2000. (bibtex) (pdf)
(ps)
 Hongwei Xi and Songtao Xia,
Towards Array Bound Check Elimination in Java Virtual Machine Language.
In Proceedings of CASCON'99, pp. 110125, Mississauga, Ontario, November 1999.
(bibtex)
(pdf)
(ps)
(slides in ppt)
 Hongwei Xi and Frank Pfenning, Dependent Types in Practical Programming.
In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'99), pp. 214227, San Antonio, January 1999.
(bibtex)
(pdf)
(ps)
 Hongwei Xi and Frank Pfenning, Eliminating Array Bound Checking Through Dependent Types.
In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'98), pp. 249257,
Montreal, June 1998.
(bibtex)
(pdf)
(ps)
 Hongwei Xi, Towards automated termination proofs through "Freezing".
In the proceedings of 9th International Conference on Rewriting Techniques and Applications (RTA'98), pp. 271285, Japan, April 1998.
(bibtex)
(pdf)
(ps)
 Hongwei Xi, Evaluation under lambdaabstraction. In Proceedings
of 9th International Symposium on Programming Languages, Implementations,
Logics, and Programs (PLILP'97), SpringerVerlage LNCS 1292, pp. 259273,
Southampton, UK, September 1997.
(bibtex) (pdf) (ps)
 Hongwei Xi, Upper bounds for standardisation and an application.
In the proceedings of Kurt GĂ¶del Colloquium 1997 (KGC'97),
SpringerVerlag LNCS, vol. 1289, pp. 335348, Vienna, August 1997.
(bibtex)
(pdf)
(ps)
 Hongwei Xi, Simulating EtaExpansions with BetaReductions in
the SecondOrder Polymorphic LambdaCalculus. In the proceedings of
Symposium on Logical Foundations of Computer Science (LFCS'97),
SpringerVerlag LNCS, vol. 1234, pp. 399409, Yaroslavl, July 1997. (bibtex) (pdf)
(ps)
 Hongwei Xi, Weak and Strong Beta Normalisations in Typed LambdaCalculi.
In the proceedings of Typed Lambda Calculi and Applications (TLCA'97),
SpringerVerlag LNCS, vol. 1210, pp. 390404, April 1997.
(bibtex)
(pdf)
(ps)
Workshops
 Zhiqiang Ren
and Hongwei Xi, A ProgrammerCentric Approach to Program
Verification in ATS, Automated Reasoning in Security and Software
Verification (a workshop with CADE24), Lake Placid, New York, June 9, 2013.
(bibtex)
(pdf) (ps)
 Matthew Danish and
Hongwei Xi, Operating System Development with ATS. In the
Proceedings of International Workshop on Programming Languages Meets
Program Verification (PLPV'10), Madrid, Spain, January, 2010.
(bibtex)
(pdf) (ps)
 Hongwei Xi, Attributive Types for Proof Erasure. In the
postworkshop proceedings of the international workshop TYPES'07, LNCS
vol. 4941, December 2007.
(bibtex)
(pdf)
(ps)

Kevin Donnelly and
Hongwei Xi, A Formalization of Strong Normalization for Simply Typed
LambdaCalculus and System F. International Workshop on Logical Frameworks and
MetaLanguages: Theory and Practice (LFMTP'06), Seattle,
WA, August 2006. (bibtex) (pdf) (ps)

Kevin Donnelly and
Hongwei Xi, System Description: Combining HigherOrder Abstract
Syntax with FirstOrder Abstract Syntax in ATS. International
Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN'05), Tallinn, Estonia,
September 2005. (bibtex) (pdf) (ps)

Sa Cui and
Kevin Donnelly and
Hongwei Xi, ATS: a language that
combines programming with theorem proving. In Proceedings of the 5th
International Workshop on Frontiers of Combining Systems, (FroCos'05),
SpringerVerlag LNCS 3717, pp. 310320,
Vienna, Austria,
September 2005. (bibtex) (pdf) (ps)
 Hongwei Xi, Development Separation in LambdaCalculus, In
Proceedings of the 12th Workshop on Logic, Language, Information and
Computation (WoLLIC'05),
ENTCS vol. 143, pp. 207221,
Florianopolis, Santa Catarina, Brazil, July 2005. (bibtex) (pdf) (ps) (slides in pdf)
 Hongwei Xi, Applied Type System (extended abstract). In the
postworkshop proceedings of
TYPES 2003,
SpringerVerlag LNCS vol. 3085, pp. 394408, 2004.
(bibtex)
(pdf)
(ps)
(full paper: pdf ps)

Chiyan Chen and
Hongwei Xi, Implementing Typeful Program Transformations, ACM
SIGPLAN 2003 Workshop on Partial Evaluation and Semantics Based Program
Manipulation (PEPM'03), pp. 2028, San Diego, CA, June 2003. (bibtex) (pdf)
(ps)
 Hongwei Xi and
Carsten
Schuermann, CPS Transform for Dependent ML (abstract). In the
meeting report of the 8th Workshop on Logic, Language, Information and
Computation (WoLLIC'01), Logic Journal of IGPL, 9(5), pp. 739754,
Brasilia, Brazil, August 2001. (bibtex)
(pdf) (ps)
 Hongwei Xi, Dependently Typed Data Structures. In Proceedings
of the Workshop on Algorithmic Aspects of Advanced Programming
Languages (WAAAPL'99), pp. 1732, Paris, September 1999. (bibtex) (pdf) (ps)
(slides in ppt)
(full paper: pdf ps)
 Hongwei Xi, Dead Code Elimination through Dependent Types.
In Proceedings of the First International Workshop on Practical Aspects of Declarative Languages(PADL'99), SpringerVerlag LNCS vol. 1551, pp.228242,
San Antonio, January 1999.
(bibtex)
(pdf)
(ps)
 Hongwei Xi, Generalized LambdaCalculi (abstract).
In the meeting report of the 4th Workshop on Logic, Language, Information and
Computation (WoLLIC'97), Logic Journal of IGPL, 5(6), pp. 925927,
Fortaleza(Ceara), Brazil, August 1997.
(bibtex)
(pdf)
(ps)
 Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning,
and Hongwei Xi,
TPS: An interactive and automatic tool for proving theorems of type theory,
In Jeffrey J. Joyce and CarlJohan H. Seger, editors, Proceedings of the 6th International
Workshop on Higher Order Logic Theorem Proving and Its Applications,
pages 366370, Vancouver, B.C., Canada, August 1993. SpringerVerlag LNCS 780.
(bibtex) (ps)
 Hongwei Xi,
On branching and nonbranching recursively enumerable degrees (in Chinese),
National Logic Workshop,
Shantou University, China, October, 1990.
Invited Papers
 Hongwei Xi, ATS/LF: a type system for constructing proofs as
total functional programs. In the Festschrift in honor of Peter Andrews on
the occasion of his 70th birthday, Studies in Logic and the Foundation of
Mathematics, 2008.
(bibtex)
(pdf)
(ps)
 Hongwei Xi, Unifying ObjectOriented Programming with Typed
Functional Programming, ASIAN Symposium on Partial Evaluation and
SemanticsBased Program Manipulation (ASIAPEPM'02), pp. 117125,
AizuWakamatsu, Japan, September 2002. (bibtex) (pdf) (ps)
Technical Reports

Hongwei Xi and Dengping Zhu and Yanka Li, Applied Type System with
Stateful Views, Technical Report, no. BUCS200503, Computer Science
Department, Boston University, January, 2005. (pdf) (ps)
 Hongwei Xi and Joachim Steinbach, Erasure for Termination Proofs, Technical
Report OGICSE99009, Oregon Graduate Institute, August 1999.
 Hongwei Xi and Robert Harper, A
Dependently Typed Assembly Language,
Technical Report OGICSE99008,
Oregon Graduate Institute,
July 1999.
 Joachim Steinbach and Hongwei Xi, Freezing  Termination Proofs for Classical, ContextSensitive and Innermost Rewriting, January 1998
 Hongwei Xi, On weak and strong normalisations, Research Report 96187,
Mathematics Department, Carnegie Mellon University, 1996.
 Hongwei Xi, An induction measure on lambdaterms and its applications,
Research Report 96192, Mathematics Department, Carnegie Mellon University, 1996.
Manuscripts
 Hongwei Xi, Dependent Types in Practical Programming (Ph.D thesis), September, 1998
 Hongwei Xi, Combining Algebraic Rewriting with Second Order Extentional Polymorphic Lambda Calculus, October, 1996
[ Home
 Contact
 CV
 Research
 Publication
]
[ Projects
 Courses
]
hwxi AT cs DOT bu DOT edu
http://www.cs.bu.edu/~hwxi
