
Hongwei Xi
Curriculum Vitæ (txt)
Education:
PhD in Pure & Applied Logic, December 1998
Carnegie Mellon University, Pittsburgh, USA
M.S. in Mathematics, July 1988
Nanjing University, Nanjing, China
B.S. in Mathematics June 1985
Nanjing University, Nanjing, China
Academic Experience
Associate Professor, September 2007 to Present
Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215
Assistant Professor, October 2001 to August 2007
Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215
Assistant Professor, September 1999 to October 2001
Department of Electrical and Computer Engineering and Computer Science
University of Cincinnati
Cincinnati, OH 452210030
Postdoc Research Associate, August 1998 to August 1999
Pacific Software Research Center
Department of Computer Science & Engineering
Oregon Graduate Institute
Lecturer, July 1988 to June 1992
Department of Computer Science
Shanghai Jiao Tong University
Shanghai, China
PhD Thesis
 Dependent Types in Practical Programming
(pdf),
Carnegie Mellon University, pp. 189+viii, December 1998.
Grant Awards
 Hongwei Xi (PI), ATS for systems programming with
theorem proving, National Science Foundation, CCF1018601, $449,935, 20102013.
 Hongwei Xi (PI), ATS: a language to support practical programming with
theorem proving, National Science Foundation, CCF0702665, $299,980, 20072010.
 Hongwei Xi (PI),
CAREER: Realistic Program Termination Verification: Theory and Practice,
National Science Foundation, CCR0092703/0229480, $284,938, 20012007.
 Hongwei Xi (PI), Imperative Programming with Dependent Types, National
Science Foundation, CCR0081316/0224244, $334,918, 20002004.
 Paul Sivilotti and Hongwei Xi (PIs), Dependent Types for
HighConfidence Distributed Systems, Ohio Board of Regents, $89,954,
20002002.
 Hongwei Xi (PI), Faculty Development, University of Cincinnati, $3,108, 2000.
Refereed Papers
Journals

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,
Computational Biology and Chemistry 59: 98112 (2015)

Matthew Danish,
Hongwei Xi, and Richard West:
Applying languagebased static verification in an ARM operating
system. SIGBED Review 10(2): 16 (2013).
 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. (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 (JFP),
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 (HOSC), 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 (IC), 149(2),
pp. 173225, 1999. (bibtex)
(pdf) (ps)
 Hongwei Xi, Upper bounds for standardisation and an application,
Journal of Symbolic Logic (JSL), 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 (JAR), 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

Zhe Chen,
Ou Wei,
Zhiqiu Huang,
Hongwei Xi:
Formal Semantics of Runtime Monitoring, Verification,
Enforcement and Control. In Proceedings of the 9th International
Symposium on Theoretical Aspects of Software Engineering (TASE),
pp. 6370, Nanjing, China, September 1214, 2015.

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. 382392, Natal, Brazil, September 13, 2010.
(bibtex)
(pdf)
(ps)
(slides in ppt)
 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. (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)
 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),
SpringerVerlag 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, 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 the First International Conference on Software
Engineering and Formal Methods (SEFM'03), pp. 7281,
Brisbane, Australia, September 2003. (bibtex) (pdf) (ps)
 Chiyan Chen and Hongwei Xi,
MetaProgramming through Typeful Code Representation.
In Proceedings of International Conference on Functional Programming
(ICFP'03),
pp. 275286, Uppsala, Sweden, August 2003.
(bibtex)
(pdf)
(ps)
 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)
 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)
(ps)
(pdf)
(slides in ppt)
 Hongwei Xi, Unifying ObjectOriented Programming with Typed
Functional Programming. In Proceedings of the First ASIAN Symposium on Partial
Evaluation and SemanticsBased Program Manipulation (ASIAPEPM),
pp. 117125, AizuWakamatsu, Japan, September 2002. (bibtex) (pdf) (ps) (slides in ppt)
 Hongwei Xi and Robert
Harper, A Dependently Typed Assembly Language. In Proceedings of
the 6th ACM SIGPLAN International Conference on Functional Programming
(ICFP'01), pp. 169180, Florence, September 2001 (bibtex) (pdf) (ps) (slides in ppt)
 Hongwei Xi, Dependent Types for Program Termination
Verification. In Proceedings of 16th IEEE Symposium on Logic in Computer
Science (LICS'01), pp. 231242, Boston, June 2001. (bibtex) (pdf) (ps) (slides in ppt)
 Hongwei Xi,
Imperative Programming with Dependent Types.
In Proceedings of 15th IEEE Symposium on Logic in Computer Science (LICS'00),
Santa Barbara, June 2000.
(bibtex)
(pdf)
(ps)
(slides in ppt)
 Hongwei Xi and Songtao Xia,
Towards Array Bound Check Elimination in Java Virtual Machine Language.
In Proceedings of CASCON'99, Mississauga, Ontario, November 1999.
(bibtex)
(pdf)
(ps)
 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, Texas, 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 Proceedings of 9th International Conference on
Rewriting Techniques and Applications (RTA'98),
SpringerVerlag LNCS vol. 1379, 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),
SpringerVerlag LNCS vol. 1292, pp. 259273,
Southampton, UK, September 1997.
(bibtex)
(pdf)
(ps)
 Hongwei Xi, Upper bounds for standardisation and an application.
In Proceedings of Kurt Gödel Colloquium 1997 (KGC'97),
SpringerVerlag LNCS vol. 1289, pp. 335348, August 1997.
(bibtex)
(pdf)
(ps)
 Hongwei Xi, Simulating EtaExpansions with BetaReductions in the SecondOrder Polymorphic LambdaCalculus.
In 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 Proceedings of Typed Lambda Calculi and Applications (TLCA'97),
SpringerVerlag LNCS vol. 1210, pp. 390404, April 1997.
(bibtex)
(pdf)
(ps)
Workshops

Kiwamu Okabe and Hongwei Xi,
Arduino programing of MLstyle in ATS, ML Workshop at ICFP 2015.

William Blair and Hongwei Xi,
Dependent Types for RealTime Constraints, ML Workshop at ICFP 2015.
 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, 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, 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,
the 5th International Workshop on
Frontiers of Combining Systems (FroCos),
SpringerVerlag LNCS vol. 3717,
pp. 310320,
Vienna, September 2005 (bibtex) (pdf) (ps)
 Hongwei Xi, Development separation in lambdacalculus, 12th Workshop on Logic,
Language, Information and Computation (WoLLIC), Florianopolis, ENTCS
vol. 143, pp. 207221, Santa Catarina, Brazil, July, 2005. (bibtex) (pdf) (ps)
 Hongwei Xi, Applied Type System (extended abstract).
In the postworkshop proceedings of
TYPES 2003,
SpringerVerlag LNCS vol. 3085, 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
pp. 2028, (PEPM'03), 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 Workshop on Algorithmic Aspects of Advanced Programming Languages (WAAAPL'99), Paris, September 1999.
(bibtex)
(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), Logic Journal of IGPL, 5(6), pp. 925927,
Fortaleza(Ceara), Brazil, August, 1997.
 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,
SpringerVerlag LNCS vol. 780, pp. 366370, Vancouver, B.C., Canada, August 1993.
 Hongwei Xi. On branching and nonbranching recursively
enumerable degrees (in Chinese), National Logic Conference,
Shantou University, China, October, 1990.
Unrefereed Papers
Technical Reports
 Hongwei Xi and Joachim Steinbach,
Erasure for Termination Proofs, Technical Report OGICSE99009, August 1999.
(ps)
 Joachim Steinbach and Hongwei Xi.
Freezing  Termination for Classical, ContextSensitive and Innermost Rewriting,
Institut fuer Informatik, Technische Universitat Muenchen, January, 1998.
(ps)
 Hongwei Xi.
An Induction Measure on LambdaTerms and Its Applications.
Research Report 96192, Department of Mathematical Sciences, 1996.
(ps)
 Hongwei Xi.
On Weak and Strong Normalizations. Research Report 96187,
Mathematics Department, Carnegie Mellon University, 1996.
(ps)
Manuscripts
 Hongwei Xi, Combining Algebraic Rewriting with Second Order Extentional Polymorphic Lambda Calculus, October, 1996
Technical Writing
 Hongwei Xi, Programming in ATS.
(ps)
(pdf)
 Dan Nesmith, Matthew Bishop, Peter Andrews, Sunil Issar, Frank Pfenning, and Hongwei Xi,
TPS User's Manual, pp. 84+iii.
 Peter Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi and Matthew Bishop, TPS3 Facilities Guide for Programmers and Users,
pp. 238+viii.
 Frank Pfenning, Sunil Issar, Dan Nesmith, Peter Andrews, Hongwei Xi and Matthew Bishop,
ETPS User's Manual, Version for Mathematical Logic I & II, pp. 60+ii.
Conference Presentations
 Hongwei Xi and Chiyan Chen,
Combining Programming with Theorem Proving,
the 10th International Conference on Functional Programming
(ICFP'05),
Tallinn, Estonia, September 2005.
(ps)
 Hongwei Xi and Chiyan Chen,
MetaProgramming through Typeful Code Representation,
the 8th International Conference on Functional Programming
(ICFP'03),
Uppsala, Sweden, August 2003.
(ppt)
 Hongwei Xi and Chiyan Chen and Gang Chen,
Guarded Recursive Datatype Constructors,
the 30th ACM SIGPLAN Symposium on
Principles of Programming Languages (POPL'03),
New Orleans, Louisiana, January 2003.
(ppt)
 Hongwei Xi and Robert
Harper, A Dependently Typed Assembly Language, the 6th International
Conference on Functional Programming (ICFP'01), pp. 169180, Florence,
September 2001 (slides in ppt)
 Hongwei Xi, Dependent Types for Program
Termination Verification, the 16th IEEE SIGPLAN Symposium on Logic in
Computer Science (LICS'01), Boston, MA, June 2001. (slides in ppt)
 Hongwei Xi,
Imperative Programming with Dependent Types, the 15th IEEE SIGPLAN Symposium on
Logic in Computer Science (LICS'00), Santa Barbara, CA, June 2000.
(slides in ppt)
 Hongwei Xi and Frank
Pfenning, Dependent Types in Practical Programming, the 26th ACM
SIGPLAN Symposium on Principles of Programming Languages (POPL'99), San
Antonio, January 1999. (slides in
ps)
 Hongwei Xi, Dead Code Elimination through
Dependent Types, First International Workshop on Practical Aspects of
Declarative Languages (PADL'99), San Antonio, January, 1999.
(slides in ps)
 Hongwei Xi and Frank
Pfenning, Eliminating Array Bound Checking
through Dependent Types, ACM SIGPLAN Conference on Programming
Language Design and Implementation (PLDI'98), Montreal, June, 1998.
(slides in ps)

Matthew Bishop and Hongwei Xi, The ETPS Educational Theorem Proving
System, The 8th Annual Computing and Philosophy Conference (CAP),
Pittsburgh, August, 1993.
Invited Talks
 Hongwei Xi,
ATS as a functional programming frontend to generating highquality
embedded C code, National Software Application Conference
(NASAC'12),
Nanjing University of Aeronautics and Astronautics, Nanjing, China,
October 21, 2012. (slides in
pdf) (slides in ps)
 Hongwei Xi,
A Brief Introduction to ATS, Department of
Computer Science and Technology, Nanjing University of Aeronautics and
Astronautics, Nanjing, China, January 10, 2012.
(slides in pdf)
(slides in ps)
 Hongwei Xi, Views and Viewtypes in ATS,
Programming Language Group, CSAIL, Massachusetts Institute of Technology,
December 5, 2011.
(slides in pdf)
(slides in ps)
 Hongwei Xi, Programming with Theorem Proving (Functional Part),
University of Saarbrucken, Saarland, Germany, October 9, 2007.
(slides in pdf)
(slides in ps)
 Hongwei Xi, To memory safety through proofs and beyond, the
International Workshop of the TYPES project (TYPES'06), University of
Nottingham, United Kingdom, April 1821, 2006. (slides in pdf) (slides in ps)
 Hongwei Xi,
To memory safety through proofs, Triforce group, DEAS, Harvard University,
November 30, 2005. (slides in pdf) (slides in ps)
 Hongwei Xi, To memory safety through proofs, Sun Microsystems,
Burlington, MA, November 17, 2005. (slides in pdf) (slides in ps)
 Hongwei Xi,
Programming with C library functions safely,
Computer Science and Engineering Department, Washington University at
St. Louis, MO, November 11, 2005.
(slides in pdf)
(slides in ps)
 Hongwei Xi,
ATS: a language to make typeful programming real and fun,
Computer Science Department, Yale University, New Haven, CT, April 28, 2005.
(slides in ps)
 Hongwei Xi, Implmenting an evaluator for miniML in ATS: a case of programming with theorem proving,
Fifth International Workshop on Reduction Strategies in Rewriting and
Programming (WRS'05), Nara, Japan,
April 22, 2005. (code) (pdf) (ps) (slides in ps)
 Hongwei Xi,
Unifying ObjectOriented Programming with Typed Functional Programming,
Computer Science Department, Rice University, Houston, TX, April 16 & 18, 2003.
(ppt)
 Hongwei Xi,
Unifying ObjectOriented Programming with Typed Functional Programming,
ASIAN Symposium on Partial Evaluation and SemanticsBased Program
Manipulation (ASIAPEPM), AizuWakamatsu, Japan, September 14, 2002.
(ppt)
 Hongwei Xi, Implementing Staged Computation,
Information Processing Laboratory, Department of Information Engineering
and Department of Mathematical Science and Informatics, University of Tokyo,
Tokyo, Japan, September 11, 2002.
(ppt)
 Hongwei Xi,
Dependent Types for Program Termination Verification,
Computer Science Department, Yale University, June 13, 2001.
(ppt)
 Hongwei Xi,
Compiling with Dependent Types, Workshop on ProofCarrying Code,
Santa Barbara, CA, June 29, 2000.
(ps)
(ppt)
 Hongwei Xi,
A Dependently Typed Assembly Language, ROPAS group,
Department of Computer Science, Korea Advanced Institute of
Science and Technology (KAIST), Taejon, Korea, April 7, 1999.
(ps)
(ppt)
 Hongwei Xi,
Dependent Types in Practical Programming, ROPAS group,
Department of Computer Science, Korea Advanced Institute of
Science and Technology (KAIST), Taejon, Korea, April 6, 1999.
 Hongwei Xi,
Dependenly Typed Assembly Language,
Workshop on Dependent Types in Programming,
Göteborg, Sweden, March 2728, 1999.
(ps)
(ppt)
 Hongwei Xi, Dependent Types in Practical
Programming, Formal Methods PI meeting, Stanford University, October
1998. (ps) (ppt)
Graduate Student Supervision

Songtao Xia, PhD student, Oregon Graduate Institute, August 1998  August 1999.

Varun Nayak,
MS student, University of Cincinnati, January 2000  May
2002. (Varun successfully defended his Master's thesis titled
A Survey on Algorithms for Solving Linear Integer Type Constraints
in May 2002 and is now working for a company in London, England)

Sudeep Sabnis, MS
student, University of Cincinnati, January 2001  August 2003.
(Sudeep successfully defended his Master's thesis titled
An Approach to Facilitating Verification of Linear Constraints
in August 2003)

Chiyan Chen, PhD student,
Boston University, June 2002  August 2005.
(Chiyan successfully defended his doctoral thesis titled
Type Inference in Applied Type System on July 29, 2005)

Dengping Zhu, PhD student,
Boston University, September 2001  May 2006. (Dengping successfully
defended his Master's thesis titled Typed Stateful Programming in
April 2004) (Dengping successfully defended his doctoral thesis titled
To Memory Safety through Proofs on April 3, 2006)

Sa Cui, MS student,
Boston University, September 2002  May 2006. (Sa successfully defended
his Master's thesis titled Typeful Assembly Programming in ATS on
April 4, 2006)

Rui Shi, PhD student,
Boston University, September 2002  May 2007. (Rui successfully defended
his doctoral thesis titled Types for Safe Resource Sharing in
Sequential and Concurrent Programming on May 3, 2007)

Rick Lavoie, MS
student, Boston University, June 2005  May 2007. (Rick successfully
completed his project on building a bytecode interpreter and a native
compiler for ATS in May 2007)

Kevin Donnelly, MS
student, Boston University, September 2004  December 2007. (Kevin
successfully completed his thesis titled Strong Normalization for
System FC)

Michel Machado, MS student,
Boston University, September 2006  May 2008. (Michel successfully
completed his thesis titled Dependent Type for Strings to Avoid
Injections)

Likai Liu, PhD student,
Boston Univeristy, September 2004  May 2014. (Likai successfully defended
his doctoral thesis titled Simple, Safe, and Efficient Memory Management
Using Linear Pointers on March 27, 2014)

Matthew Danish, PhD student,
Boston Univeristy, September 2008  May 2015. (Matthew successfully
defended his doctoral thesis titled Terrier: A realtime, embedded
operating system using advanced types for safety on March 31, 2015)
Service:
PC Member 
The 13th International Symposium on Functional and Logic Programming
(FLOPS'16), Kochi, Japan, March, 2016


The 2014 ACM SIGPLAN Workshop on ML, Gothenburg, Sweden, 2014


Dependently Typed Programming (DTP 2014), Vienna, Austria, July, 2014


The 12th ASIAN
Symposium on Programming Languages and Systems (APLAS'14), Singapore, 2014


The Eighth ASIAN
Symposium on Programming Languages and Systems (APLAS'10), Shanghai, China, 2010


The 2008 ACM SIGPLAN
Workshop on ML, Victoria, British Columbia, Canada, September 21st, 2008


The 3rd workshop on
Logic and Semantic Frameworks, with Applications (LSFA'08),
San Salvador, Brazil, August 26th, 2008


ACM SIGPLAN Conference on Programming
Language Design and Implementation (PLDI'08), Tucson, AZ, June, 2008


The 2nd workshop on
Programming Languages meet Program Verification (PLPV'07), Freiberg,
Germany, October, 2007 (CoChair with Aaron Stump)


The 1st workshop on
Programming Languages meet Program Verification (PLPV'06), Seattle,
Washington, August, 2006 (CoChair with Aaron Stump)


The 2nd workshop on
Logic and Semantic Frameworks, with Applications (LFSA'07),
Ouro Preto, Brazil, August 28th, 2007.


The 2nd International Conference
on Software and Data Technologies (ICSOFT), Barcelona, Spain, July
2225, 2007.


The ACM SIGPLAN
Workshop on Types in Language Design and Implementation (TLDI'07),
Nice, France, January 16, 2007.


The 11th International
Conference on Functional Programming (ICFP'06), Portland, Oregon,
September 1820, 2006.


The 1st International Conference
on Software and Data Technologies (ICSOFT), Setubal, Portugal, September
1114, 2006.


The 1st workshop on
Programming Languages meet Program Verification (PLPV'06), Seattle,
Washington, August, 2006 (CoChair with Aaron Stump)


The 33rd ACM
SIGPLANSIGACT Symposium on Principles of Progamming Languages
(POPL'06), Charleston, South Carolina, January 1113, 2006


The Second International
Conference on Embedded Software and Systems (ICESS'05),
Xi'an, China, Dec 1618, 2005


The Second MetaOCaml
Workshop, Tallin, Estonia, September 28, 2005


The 15th New England Programming Language and Systems (NEPLS), June, 2005


The 14th New England Programming
Language and Systems (NEPLS), February, 2005
(coorganized with Assaf Kfoury)


The Second ASIAN
Symposium on Progamming Languages and Systems (APLAS 2004), Taipei,
Taiwan, November 46, 2004


The First MetaOCaml
Workshop, Vancouver, BC, Canada, October 25, 2004



Referee 
Functional and Logic Programming (FLOPS) (2016) 

Typed LambdaCalculus and Applications (TLCA) (2015, 2007, 2005) 

Dependently Typed Programming (DTP 2014) 

Asian Symposium on Programming Languages and Systems (2014, 2010, 2004, 2003) 

Transaction on Programming Languages and Systems (TOPLAS) (2012, 2009, 2005, 2004, 2003, 2001) 

Symposium on Principles of Programming Languages (POPL) (2012, 2008, 2007, 2006, 2005, 2004, 2003) 

Journal of Mathematical Structures in Computer Sciences (MSCS) (2011) 

Journal of Functional Programming (JFP) (2009, 2007, 2005, 2004, 2001) 

International Workshop on Programming Language meets Programming Verification (PLPV) (2009) 

ACM International Conference on Functional Programming (ICFP) (2008, 2006, 2004, 2003, 2002, 1998) 

European Symposium on Programming (ESOP) (2008, 2007, 2006, 2003) 

Compiler Construction (CC) (2008) 

Types in Language Design and Implementation (TLDI) (2007) 

Foundations of Software Science and Computation Structures (FoSSaCS) (2007) 

IEEE Symposium on Logic in Computer Science (LICS) (2007, 2005, 2003, 2002, 2000) 

International Conference on Rewriting Techniques and Applications (RTA) (2007, 2006) 

International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR) (2006) 

ACM Transactions on Architecture and Code Optimization (TACO) (2006) 

International Colloquium on Automata, Languages and Programming (ICALP) (2006, 2005) 

RealTime Systems Symposium (RTSS) (2005) 

Computer Science Logic (CSL) (2005) 

Journal of Science of Computer Programming (SCP) (2005) 

Practical Aspects of Declarative Languages (PADL) (2005) 

Journal of HigherOrder Symbolic Computation (HOSC) (2004, 2001, 2000, 1999) 

Journal of Automated Reasoning (2004, 2003, 2002) 

RealTime and Embedded Technology and Applications Symposium (RTAS) (2004) 

TYPES'03 Workshop (2003) 

The Bulletin of Symbolic Logic (2003) 

Haskell Workshop (2003) 

International Computing and Combinatorics Conference (COCOON) (2003) 

Workshop on Programs as Data Objects (PADO) (2000) 

The First International Conference on Parallel and
Distributed Computing, Applications and Technologies (PDCAT) (2000) 

CSER (Consortium for Software Engineering Research) Book (2000) 

Journal of Information and Computation (1996) 


[ Home
 Contact
 CV
 Research
 Publications
]
[ Projects
 Courses
]
hwxi AT cs DOT bu DOT edu
http://www.cs.bu.edu/~hwxi
