Hongwei Xi
Curriculum Vitæ (txt)

Education:

Academic Experience

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, CCF-1018601, $449,935, 2010-2013.

• Hongwei Xi (PI), ATS: a language to support practical programming with theorem proving, National Science Foundation, CCF-0702665, $299,980, 2007-2010.

• Hongwei Xi (PI), CAREER: Realistic Program Termination Verification: Theory and Practice, National Science Foundation, CCR-0092703/0229480, $284,938, 2001-2007.

• Hongwei Xi (PI), Imperative Programming with Dependent Types, National Science Foundation, CCR-0081316/0224244, $334,918, 2000-2004.

• Paul Sivilotti and Hongwei Xi (PIs), Dependent Types for High-Confidence Distributed Systems, Ohio Board of Regents, $89,954, 2000-2002.

• Hongwei Xi (PI), Faculty Development, University of Cincinnati, $3,108, 2000.

Refereed Papers

Journals

1. Leonard Kosta, John Irvine, Laura Seaman, Hongwei Xi, Many-target, Many-sensor Ship Tracking and Classification. HPEC 2019: 1-7, 2019.

2. Leonard Kosta, Laura Seaman, Hongwei Xi, Program Synthesis and Vulnerability Injection Using a Grammar VAE. J. Software 14(6): 227-246 (2019)

3. 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: 98-112 (2015)

4. Matthew Danish, Hongwei Xi, and Richard West: Applying language-based static verification in an ARM operating system. SIGBED Review 10(2): 16 (2013).

5. Rui Shi and Hongwei Xi, A Linear Type System for Multicore Programming, Science of Computer Programming, 2012.

6. Hongwei Xi, Dependent ML: an approach to practical programming with dependent types, Journal of Functional Programming (JFP), vol. 17(2), pp. 215-286, 2007. (pdf) (ps)

7. Chiyan Chen, Rui Shi and Hongwei Xi, Implementing Typeful Program Transformations, Fundamenta Informaticae, vol. 69 (1-2), pp. 103-121, 2005 (bibtex) (pdf) (ps)

8. Chiyan Chen and Hongwei Xi, Meta-Programming through Typeful Code Representation, Journal of Functional Programming (JFP), vol. 15(6), pp. 797--835, 2005. (bibtex) (pdf) (ps)

9. 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. 75--92, 2004. (pdf) (ps)

10. Hongwei Xi, Dependently Typed Pattern Matching, Journal of Universal Computer Science (JUCS), 9(8), pp. 851-872, August 2003. (bibtex) (pdf) (ps)

11. Hongwei Xi, Dependent Types for Program Termination Verification, Journal of Higher-Order Symbolic Computation (HOSC), 15(1), pp. 91--131, March 2002. (bibtex) (pdf) (ps)

12. Femke van Raamsdonk, Paula Severi, Morten H. Sorensen and Hongwei Xi, Perpetual Reductions in Lambda-Calculus, Journal of Information and Computation (IC), 149(2), pp. 173--225, 1999. (bibtex) (pdf) (ps)

13. Hongwei Xi, Upper bounds for standardisation and an application, Journal of Symbolic Logic (JSL), 64(1), pp. 291--303, March 1999. (bibtex) (pdf) (ps)

14. 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. 321--353, 1996. (bibtex) (pdf)

15. Hongwei Xi, Half-Closed Intervals of Rescursively Enumerable Degrees (in Chinese with English abstract), Math. Semiannuals of Nanjing University, P.R. China, 1989.
    

Conferences and Symposiums

1. William Blair and Hongwei Xi: Dependent Types for Multi-Rate Flows in Synchronous Programming. CoRR abs/1702.02282 (2017)

2. Zhiqiang Ren and Hongwei Xi: Combining Type-Checking with Model-Checking for System Verification. In Proceedings of MEMOCODE 2016: pp. 54-58, Kanpur, India, November 18-20, 2016.

3. Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi, and Zhibin Yang: Parametric Runtime Verification of C Programs. In Proceedings of TACAS 2016: pp. 299-315, Eindhoven, The Netherlands, April 2-8, 2016.

4. Zhe Chen, Ou Wei, Zhiqiu Huang, and 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. 63-70, Nanjing, China, September 12-14, 2015.

5. 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)

6. 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. 382-392, Natal, Brazil, September 1-3, 2010. (bibtex) (pdf) (ps) (slides in ppt)

7. 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. 336-349, Gramado, Brazil, August 19-21, 2009. (bibtex) (pdf) (ps) (slides in ps) (slides in pdf)

8. 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 19-21, 2009. (bibtex) (pdf) (ps) (slides in ps) (slides in pdf)

9. Rui Shi, Chiyan Chen and Hongwei Xi, Distributed Meta-Programming. 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)

10. Chiyan Chen and Hongwei Xi, Combining Programming with Theorem Proving. In Proceedings of the 10th International Conference on Functional Programming (ICFP'05), pp. 66--77, Tallinn, Estonia, September 2005. (pdf) (ps) (slides in pdf)

11. 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), Springer-Verlag LNCS vol. 3350, pp. 83--97, Long Beach, CA, January 2005. (bibtex) (pdf) (ps)

12. Chiyan Chen, Rui Shi and Hongwei Xi, A Typeful Approach to Object-Oriented Programming with Multiple Inheritance. In Proceedings of the 6th International Symposium on Practical Aspects of Declarative Languages (PADL'04), Springer-Verlag LNCS vol. 3057, pp. 23--38, Dallas, TX, June 2004. (bibtex) (pdf) (ps) (slides in ppt)

13. 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), Springer-Verlag LNCS vol. 3057, pp. 239--254, Dallas, TX, June 2004. (bibtex) (pdf) (ps) (slides in ppt)

14. 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), Springer-Verlag LNCS vol. 2895, Beijing, China, November 2003. (bibtex) (pdf) (ps)

15. Walid Taha, Stephan Ellner and Hongwei Xi, Generating Imperative, Heap-Bounded Programs in a Functional Setting. In Proceedings of the Third International Conference on Embedded Software (EMSOFT'03), Springer-Verlag LNCS vol. 2855, pp. 340-355, Philadelphia, PA, October 2003. (bibtex) (pdf) (ps)

16. Hongwei Xi, Facilitating Program Verification with Dependent Types. In Proceedings of the First International Conference on Software Engineering and Formal Methods (SEFM'03), pp. 72--81, Brisbane, Australia, September 2003. (bibtex) (pdf) (ps)

17. Chiyan Chen and Hongwei Xi, Meta-Programming through Typeful Code Representation. In Proceedings of International Conference on Functional Programming (ICFP'03), pp. 275--286, Uppsala, Sweden, August 2003. (bibtex) (pdf) (ps)

18. Hongwei Xi, Dependently Typed Pattern Matching. In Proceedings of Simposio Brasileiro de Linguagens de Programacao (SBLP'03), pp. 149--165, Ouro Preto, Brazil, May 2003. (bibtex) (pdf) (ps)

19. 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. 224--235, New Orleans, Louisiana, January 2003. (bibtex) (ps) (pdf) (slides in ppt)

20. Hongwei Xi, Unifying Object-Oriented Programming with Typed Functional Programming. In Proceedings of the First ASIAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (ASIA-PEPM), pp. 117--125, Aizu-Wakamatsu, Japan, September 2002. (bibtex) (pdf) (ps) (slides in ppt)

21. 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. 169--180, Florence, September 2001 (bibtex) (pdf) (ps) (slides in ppt)

22. Hongwei Xi, Dependent Types for Program Termination Verification. In Proceedings of 16th IEEE Symposium on Logic in Computer Science (LICS'01), pp. 231--242, Boston, June 2001. (bibtex) (pdf) (ps) (slides in ppt)

23. 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)

24. 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)

25. Hongwei Xi and Frank Pfenning, Dependent Types in Practical Programming. In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'99), pp. 214--227, San Antonio, Texas, January 1999. (bibtex) (pdf) (ps)

26. 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. 249--257, Montreal, June 1998. (bibtex) (pdf) (ps)

27. Hongwei Xi, Towards automated termination proofs through "Freezing". In Proceedings of 9th International Conference on Rewriting Techniques and Applications (RTA'98), Springer-Verlag LNCS vol. 1379, pp. 271--285, Japan, April 1998. (bibtex) (pdf) (ps)

28. Hongwei Xi, Evaluation under lambda-abstraction. In Proceedings of 9th International Symposium on Programming Languages, Implementations, Logics, and Programs (PLILP'97), Springer-Verlag LNCS vol. 1292, pp. 259--273, Southampton, UK, September 1997. (bibtex) (pdf) (ps)

29. Hongwei Xi, Upper bounds for standardisation and an application. In Proceedings of Kurt Gödel Colloquium 1997 (KGC'97), Springer-Verlag LNCS vol. 1289, pp. 335--348, August 1997. (bibtex) (pdf) (ps)

30. Hongwei Xi, Simulating Eta-Expansions with Beta-Reductions in the Second-Order Polymorphic Lambda-Calculus. In Proceedings of Symposium on Logical Foundations of Computer Science (LFCS'97), Springer-Verlag, LNCS vol. 1234, pp. 399--409, Yaroslavl, July 1997. (bibtex) (pdf) (ps)

31. Hongwei Xi, Weak and Strong Beta Normalisations in Typed Lambda-Calculi. In Proceedings of Typed Lambda Calculi and Applications (TLCA'97), Springer-Verlag LNCS vol. 1210, pp. 390--404, April 1997. (bibtex) (pdf) (ps)

Workshops

1. Hanwen Wu and Hongwei Xi, Implementing Linking in Multiparty Sessions, AGERE! 2018, November 05–07, 2018, Boston, MA, USA
2. Hongwei Xi and Hanwen Wu, Multirole Logic and Multiparty Channels, RADICAL 2017, Recent Advances in Concurrency and Logic. Berlin (Germany), September 4, 2017.
3. Hongwei Xi and Hanwen Wu, Multirole Logic (Extended Abstract), Logic Colloquium (2017), Stockholm, Sweden, August 14-20.
4. Kiwamu Okabe and Hongwei Xi, Arduino programing of ML-style in ATS, ML Workshop at ICFP 2015, Vancouver, British Columbia, Canada; August 31 – September 2, 2015
5. William Blair and Hongwei Xi, Dependent Types for Real-Time Constraints, ML Workshop at ICFP 2015.
6. Zhiqiang Ren and Hongwei Xi, A Programmer-Centric 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)

7. 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)

8. Hongwei Xi, Attributive Types for Proof Erasure. In the Post-Workshop Proceedings of the International Workshop TYPES'07, LNCS vol. 4941, December 2007. (bibtex) (pdf) (ps)

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

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

11. 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), Springer-Verlag LNCS vol. 3717, pp. 310--320, Vienna, September 2005 (bibtex) (pdf) (ps)

12. Hongwei Xi, Development separation in lambda-calculus, 12th Workshop on Logic, Language, Information and Computation (WoLLIC), Florianopolis, ENTCS vol. 143, pp. 207--221, Santa Catarina, Brazil, July, 2005. (bibtex) (pdf) (ps)

13. Hongwei Xi, Applied Type System (extended abstract). In the post-workshop proceedings of TYPES 2003, Springer-Verlag LNCS vol. 3085, 394--408, 2004. (bibtex) (pdf) (ps) (full paper: pdf ps)

14. Chiyan Chen and Hongwei Xi, Implementing Typeful Program Transformations, ACM SIGPLAN 2003 Workshop on Partial Evaluation and Semantics Based Program Manipulation pp. 20--28, (PEPM'03), San Diego, CA, June 2003. (bibtex) (pdf) (ps)

15. 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. 739--754, Brasilia, Brazil, August 2001. (bibtex) (pdf) (ps)

16. 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)

17. Hongwei Xi, Dead Code Elimination through Dependent Types. In Proceedings of the First International Workshop on Practical Aspects of Declarative Languages(PADL'99), Springer-Verlag LNCS vol. 1551, pp. 228--242, San Antonio, January 1999. (bibtex) (pdf) (ps)

18. Hongwei Xi, Generalized Lambda-Calculi (abstract), In the meeting report of the 4th Workshop on Logic, Language, Information and Computation (WoLLIC), Logic Journal of IGPL, 5(6), pp. 925--927, Fortaleza(Ceara), Brazil, August, 1997.

19. 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 Carl-Johan H. Seger, editors, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, Springer-Verlag LNCS vol. 780, pp. 366--370, Vancouver, B.C., Canada, August 1993.

20. Hongwei Xi. On branching and nonbranching recursively enumerable degrees (in Chinese), National Logic Conference, Shantou University, China, October, 1990.

Unrefereed Papers

Technical Reports

1. Hongwei Xi, Hanwen Wu: Propositions in Linear Multirole Logic as Multiparty Session Types. CoRR abs/1611.08888 (2016)
2. Hongwei Xi, Hanwen Wu: Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions. CoRR abs/1604.03020 (2016)
3. Hongwei Xi, Zhiqiang Ren, Hanwen Wu, William Blair: Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus. CoRR abs/1603.03727 (2016)
4. Hongwei Xi and Joachim Steinbach, Erasure for Termination Proofs, Technical Report OGI-CSE-99-009, August 1999. (ps)

5. Joachim Steinbach and Hongwei Xi. Freezing -- Termination for Classical, Context-Sensitive and Innermost Rewriting, Institut fuer Informatik, Technische Universitat Muenchen, January, 1998. (ps)

6. Hongwei Xi. An Induction Measure on Lambda-Terms and Its Applications. Research Report 96-192, Department of Mathematical Sciences, 1996. (ps)

7. Hongwei Xi. On Weak and Strong Normalizations. Research Report 96-187, Mathematics Department, Carnegie Mellon University, 1996. (ps)

Manuscripts

1. Hongwei Xi, Combining Algebraic Rewriting with Second Order Extentional Polymorphic Lambda Calculus, October, 1996

Technical Writing

1. Hongwei Xi, Programming in ATS. (ps) (pdf)

2. Dan Nesmith, Matthew Bishop, Peter Andrews, Sunil Issar, Frank Pfenning, and Hongwei Xi, TPS User's Manual, pp. 84+iii.

3. Peter Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi and Matthew Bishop, TPS3 Facilities Guide for Programmers and Users, pp. 238+viii.

4. 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

1. Hongwei Xi and Chiyan Chen, Combining Programming with Theorem Proving, the 10th International Conference on Functional Programming (ICFP'05), Tallinn, Estonia, September 2005. (ps)

2. Hongwei Xi and Chiyan Chen, Meta-Programming through Typeful Code Representation, the 8th International Conference on Functional Programming (ICFP'03), Uppsala, Sweden, August 2003. (ppt)

3. 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)

4. Hongwei Xi and Robert Harper, A Dependently Typed Assembly Language, the 6th International Conference on Functional Programming (ICFP'01), pp. 169--180, Florence, September 2001 (slides in ppt)

5. 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)

6. 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)

7. 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)

8. 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)

9. 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)

10. 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 front-end to generating high-quality 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 18-21, 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 mini-ML 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 Object-Oriented Programming with Typed Functional Programming, Computer Science Department, Rice University, Houston, TX, April 16 & 18, 2003. (ppt)

• Hongwei Xi, Unifying Object-Oriented Programming with Typed Functional Programming, ASIAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (ASIA-PEPM), Aizu-Wakamatsu, 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 Proof-Carrying 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 27-28, 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 real-time, embedded operating system using advanced types for safety on March 31, 2015)
• Zhiqiang (Alex) Ren, PhD student, Boston Univeristy, September 2009 - May 2017. (Zhiqiang successfully defended his doctoral thesis titled Combining Type-Checking with Model-Checking for System Verification on November 30, 2016)
• Hanwen (Steinway) Wu, PhD student, Boston Univeristy, September 2012 - May 2019. (Hanwen successfully defended his doctoral thesis titled Session Types in Practical Programming on August 30, 2018)
• Leonard Raymond Kosta, MS student, Boston University, September 2017 - May 2019. (Leo sucessfully defended his Master's thesis titled Program synthesis and vulnerability injection using a Grammar VAE on August 15, 2019)

Service:

[ Home | Contact | CV | Research | Publications ]
[ Projects | Courses ]

hwxi AT cs DOT bu DOT edu
http://www.cs.bu.edu/~hwxi