@inproceedings{XiP98,
  title = {Eliminating Array Bound Checking Through Dependent Types},
  author = {Hongwei Xi and Frank Pfenning},
  year = {1998},
  tags = {type checking},
  researchr = {https://researchr.org/publication/XiP98},
  cites = {0},
  citedby = {0},
  pages = {249-257},
  booktitle = {PLDI},
}

@inproceedings{ChenZX04,
  title = {Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell},
  author = {Chiyan Chen and Dengping Zhu and Hongwei Xi},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3057&spage=239},
  tags = {case study, Haskell},
  researchr = {https://researchr.org/publication/ChenZX04},
  cites = {0},
  citedby = {0},
  pages = {239-254},
  booktitle = {Practical Aspects of Declarative Languages, 6th International Symposium, PADL 2004, Dallas, TX, USA, June 18-19, 2004, Proceedings},
  editor = {Bharat Jayaraman},
  volume = {3057},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-22253-7},
}

@article{Xi02,
  title = {Dependent Types for Program Termination Verification},
  author = {Hongwei Xi},
  year = {2002},
  tags = {program verification, termination},
  researchr = {https://researchr.org/publication/Xi02},
  cites = {0},
  citedby = {0},
  journal = {Higher-Order and Symbolic Computation},
  volume = {15},
  number = {1},
  pages = {91-131},
}

@inproceedings{ShiCX06,
  title = {Distributed meta-programming},
  author = {Rui Shi and Chiyan Chen and Hongwei Xi},
  year = {2006},
  doi = {10.1145/1173706.1173743},
  url = {http://doi.acm.org/10.1145/1173706.1173743},
  tags = {meta programming, meta-model, programming, Meta-Environment, meta-objects},
  researchr = {https://researchr.org/publication/ShiCX06},
  cites = {0},
  citedby = {0},
  pages = {243-248},
  booktitle = {Generative Programming and Component Engineering, 5th International Conference, GPCE 2006, Portland, Oregon, USA, October 22-26, 2006, Proceedings},
  editor = {Stan Jarzabek and Douglas C. Schmidt and Todd L. Veldhuizen},
  publisher = {ACM},
  isbn = {1-59593-237-2},
}

@inproceedings{Xi97:0,
  title = {Weak and Strong Beta Normalisations in Typed Lambda-Calculi},
  author = {Hongwei Xi},
  year = {1997},
  researchr = {https://researchr.org/publication/Xi97%3A0},
  cites = {0},
  citedby = {0},
  pages = {390-404},
  booktitle = {Typed Lambda Calculi and Applications, Third International Conference on Typed Lambda Calculi and Applications, TLCA  97, Nancy, France, April 2-4, 1997, Proceedings},
  editor = {Philippe de Groote},
  volume = {1210},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-62688-3},
}

@inproceedings{Xi01,
  title = {Dependent Types for Program Termination Verification},
  author = {Hongwei Xi},
  year = {2001},
  tags = {program verification, termination},
  researchr = {https://researchr.org/publication/Xi01},
  cites = {0},
  citedby = {0},
  pages = {231-242},
  booktitle = {LICS},
}

@inproceedings{Xi02:0,
  title = {Unifying object-oriented programming with typed functional programming},
  author = {Hongwei Xi},
  year = {2002},
  doi = {10.1145/568173.568186},
  url = {http://doi.acm.org/10.1145/568173.568186},
  tags = {object-oriented programming, meta programming, functional programming, programming, subject-oriented programming, Meta-Environment, feature-oriented programming, meta-objects},
  researchr = {https://researchr.org/publication/Xi02%3A0},
  cites = {0},
  citedby = {0},
  pages = {117-125},
  booktitle = {ASIA-PEPM},
}

@inproceedings{Xi97,
  title = {Simulating eta-expansions with beta-reductions in the Second-Order Polymorphic lambda-calculus},
  author = {Hongwei Xi},
  year = {1997},
  researchr = {https://researchr.org/publication/Xi97},
  cites = {0},
  citedby = {0},
  pages = {399-409},
  booktitle = {Logical Foundations of Computer Science, 4th International Symposium, LFCS 97, Yaroslavl, Russia, July 6-12, 1997, Proceedings},
  editor = {Sergei I. Adian and Anil Nerode},
  volume = {1234},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-63045-7},
}

@inproceedings{Xi98,
  title = {Towards Automated Termination Proofs through "Freezing"},
  author = {Hongwei Xi},
  year = {1998},
  url = {http://link.springer.de/link/service/series/0558/bibs/1379/13790271.htm},
  tags = {termination},
  researchr = {https://researchr.org/publication/Xi98},
  cites = {0},
  citedby = {0},
  pages = {271-285},
  booktitle = {Rewriting Techniques and Applications, 9th International Conference, RTA-98, Tsukuba, Japan, March 30 - April 1, 1998, Proceedings},
  editor = {Tobias Nipkow},
  volume = {1379},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-64301-X},
}

@article{Xi99:0,
  title = {Upper Bounds for Standardizations and An Application},
  author = {Hongwei Xi},
  year = {1999},
  researchr = {https://researchr.org/publication/Xi99%3A0},
  cites = {0},
  citedby = {0},
  journal = {Journal of Symbolic Logic},
  volume = {64},
  number = {1},
  pages = {291-303},
}

@inproceedings{ChenX05,
  title = {Combining programming with theorem proving},
  author = {Chiyan Chen and Hongwei Xi},
  year = {2005},
  doi = {10.1145/1086365.1086375},
  url = {http://doi.acm.org/10.1145/1086365.1086375},
  tags = {programming},
  researchr = {https://researchr.org/publication/ChenX05},
  cites = {0},
  citedby = {0},
  pages = {66-77},
  booktitle = {Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005},
  editor = {Olivier Danvy and Benjamin C. Pierce},
  publisher = {ACM},
  isbn = {1-59593-064-7},
}

@inproceedings{DonnellyX05,
  title = {Combining higher-order abstract syntax with first-order abstract syntax in ATS},
  author = {Kevin Donnelly and Hongwei Xi},
  year = {2005},
  doi = {10.1145/1088454.1088462},
  url = {http://doi.acm.org/10.1145/1088454.1088462},
  tags = {abstract syntax},
  researchr = {https://researchr.org/publication/DonnellyX05},
  cites = {0},
  citedby = {0},
  pages = {58-63},
  booktitle = {ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005},
  editor = {Randy Pollack},
  publisher = {ACM},
}

@inproceedings{Xi03:0,
  title = {Facilitating Program Verification with Dependent Types},
  author = {Hongwei Xi},
  year = {2003},
  url = {http://csdl.computer.org/comp/proceedings/sefm/2003/1949/00/19490072abs.htm},
  tags = {program verification},
  researchr = {https://researchr.org/publication/Xi03%3A0},
  cites = {0},
  citedby = {0},
  pages = {72-81},
  booktitle = {1st International Conference on Software Engineering and Formal Methods (SEFM 2003), 22-27 September 2003, Brisbane, Australia},
  publisher = {IEEE Computer Society},
  isbn = {0-7695-1949-0},
}

@inproceedings{ChenX03,
  title = {Meta-programming through typeful code representation},
  author = {Chiyan Chen and Hongwei Xi},
  year = {2003},
  doi = {10.1145/944705.944730},
  url = {http://doi.acm.org/10.1145/944705.944730},
  tags = {meta programming, meta-model, programming, Meta-Environment, meta-objects},
  researchr = {https://researchr.org/publication/ChenX03},
  cites = {0},
  citedby = {0},
  pages = {275-286},
  booktitle = {Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003},
  editor = {Colin Runciman and Olin Shivers},
  publisher = {ACM},
  isbn = {1-58113-756-7},
}

@article{ChenX05:0,
  title = {Meta-programming through typeful code representation},
  author = {Chiyan Chen and Hongwei Xi},
  year = {2005},
  doi = {10.1017/S0956796805005617},
  url = {http://dx.doi.org/10.1017/S0956796805005617},
  tags = {meta programming, meta-model, programming, Meta-Environment, meta-objects},
  researchr = {https://researchr.org/publication/ChenX05%3A0},
  cites = {0},
  citedby = {0},
  journal = {Journal of Functional Programming},
  volume = {15},
  number = {5},
  pages = {797-835},
}

@inproceedings{Xi07:1,
  title = {Attributive Types for Proof Erasure},
  author = {Hongwei Xi},
  year = {2007},
  doi = {10.1007/978-3-540-68103-8_13},
  url = {http://dx.doi.org/10.1007/978-3-540-68103-8_13},
  researchr = {https://researchr.org/publication/Xi07%3A1},
  cites = {0},
  citedby = {0},
  pages = {188-202},
  booktitle = {Types for Proofs and Programs, International Conference, TYPES 2007, Cividale des Friuli, Italy, May 2-5, 2007, Revised Selected Papers},
  editor = {Marino Miculan and Ivan Scagnetto and Furio Honsell},
  volume = {4941},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-540-68084-0},
}

@article{AndrewsBINPX96,
  title = {TPS: A Theorem-Proving System for Classical Type Theory},
  author = {Peter B. Andrews and Matthew Bishop and Sunil Issar and Dan Nesmith and Frank Pfenning and Hongwei Xi},
  year = {1996},
  tags = {type system, type theory},
  researchr = {https://researchr.org/publication/AndrewsBINPX96},
  cites = {0},
  citedby = {0},
  journal = {Journal of Automated Reasoning},
  volume = {16},
  number = {3},
  pages = {321-353},
}

@inproceedings{XiP99,
  title = {Dependent Types in Practical Programming},
  author = {Hongwei Xi and Frank Pfenning},
  year = {1999},
  doi = {10.1145/292540.292560},
  url = {http://doi.acm.org/10.1145/292540.292560},
  tags = {programming},
  researchr = {https://researchr.org/publication/XiP99},
  cites = {0},
  citedby = {0},
  pages = {214-227},
  booktitle = {POPL},
}

@inproceedings{ZhuX05,
  title = {Safe Programming with Pointers Through Stateful Views},
  author = {Dengping Zhu and Hongwei Xi},
  year = {2005},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3350&spage=83},
  tags = {programming},
  researchr = {https://researchr.org/publication/ZhuX05},
  cites = {0},
  citedby = {0},
  pages = {83-97},
  booktitle = {Practical Aspects of Declarative Languages, 7th International Symposium, PADL 2005, Long Beach, CA, USA, January 10-11, 2005, Proceedings},
  editor = {Manuel V. Hermenegildo and Daniel Cabeza},
  volume = {3350},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-24362-3},
}

@inproceedings{Xi97:2,
  title = {Evaluation Under Lambda Abstraction},
  author = {Hongwei Xi},
  year = {1997},
  tags = {abstraction},
  researchr = {https://researchr.org/publication/Xi97%3A2},
  cites = {0},
  citedby = {0},
  pages = {259-273},
  booktitle = {Programming Languages: Implementations, Logics, and Programs, 9th International Symposium, PLILP 97, Including a Special Trach on Declarative Programming Languages in Education, Southampton, UK, September 3-5, 1997, Proceedings},
  editor = {Hugh Glaser and Pieter H. Hartel and Herbert Kuchen},
  volume = {1292},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-63398-7},
}

@article{RaamsdonkSSX99,
  title = {Perpetual Reductions in Lambda-Calculus},
  author = {Femke van Raamsdonk and Paula Severi and Morten Heine Sørensen and Hongwei Xi},
  year = {1999},
  researchr = {https://researchr.org/publication/RaamsdonkSSX99},
  cites = {0},
  citedby = {0},
  journal = {Inf. Comput.},
  volume = {149},
  number = {2},
  pages = {173-225},
}

@inproceedings{XiX99,
  title = {Towards array bound check elimination in Java :::TM::: virtual machine language},
  author = {Hongwei Xi and Songtao Xia},
  year = {1999},
  doi = {10.1145/781995.782009},
  url = {http://doi.acm.org/10.1145/781995.782009},
  tags = {Java},
  researchr = {https://researchr.org/publication/XiX99},
  cites = {0},
  citedby = {0},
  pages = {14},
  booktitle = {Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative Research, November 8-11, 1999, Mississauga, Ontario, Canada},
  editor = {Stephen A. MacKay and J. Howard Johnson},
  publisher = {IBM},
}

@inproceedings{TahaEX03,
  title = {Generating Heap-Bounded Programs in a Functional Setting},
  author = {Walid Taha and Stephan Ellner and Hongwei Xi},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2855&spage=340},
  tags = {functional programming},
  researchr = {https://researchr.org/publication/TahaEX03},
  cites = {0},
  citedby = {0},
  pages = {340-355},
  booktitle = {Embedded Software, Third International Conference, EMSOFT 2003, Philadelphia, PA, USA, October 13-15, 2003, Proceedings},
  editor = {Rajeev Alur and Insup Lee},
  volume = {2855},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-20223-4},
}

@article{Xi06,
  title = {Development Separation in Lambda-Calculus},
  author = {Hongwei Xi},
  year = {2006},
  doi = {10.1016/j.entcs.2005.07.014},
  url = {http://dx.doi.org/10.1016/j.entcs.2005.07.014},
  researchr = {https://researchr.org/publication/Xi06},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {143},
  pages = {207-221},
}

@inproceedings{Xi97:1,
  title = {Upper Bounds for Standardizations and an Application},
  author = {Hongwei Xi},
  year = {1997},
  researchr = {https://researchr.org/publication/Xi97%3A1},
  cites = {0},
  citedby = {0},
  pages = {335-348},
  booktitle = {Computational Logic and Proof Theory, 5th Kurt Gödel Colloquium, KGC 97, Vienna, Austria, August 25-29, 1997, Proceedings},
  editor = {Georg Gottlob and Alexander Leitsch and Daniele Mundici},
  volume = {1289},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-63385-5},
}

@inproceedings{Xi03,
  title = {Applied Type System: Extended Abstract},
  author = {Hongwei Xi},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3085&spage=394},
  tags = {type system},
  researchr = {https://researchr.org/publication/Xi03},
  cites = {0},
  citedby = {0},
  pages = {394-408},
  booktitle = {Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers},
  editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
  volume = {3085},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-22164-6},
}

@inproceedings{AndrewsBINPX93,
  title = {TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory},
  author = {Peter B. Andrews and Matthew Bishop and Sunil Issar and Dan Nesmith and Frank Pfenning and Hongwei Xi},
  year = {1993},
  tags = {type theory},
  researchr = {https://researchr.org/publication/AndrewsBINPX93},
  cites = {0},
  citedby = {0},
  pages = {366-370},
  booktitle = {Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG  93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings},
  editor = {Jeffrey J. Joyce and Carl-Johan H. Seger},
  volume = {780},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-57826-9},
}

@inproceedings{XiH01,
  title = {A Dependently Typed Assembly Language},
  author = {Hongwei Xi and Robert Harper},
  year = {2001},
  researchr = {https://researchr.org/publication/XiH01},
  cites = {0},
  citedby = {0},
  pages = {169-180},
  booktitle = {Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming},
  series = {ICFP '01},
  address = {New York, NY, USA},
  publisher = {Association for Computing Machinery},
}

@inproceedings{ZhuX03,
  title = {A Typeful and Tagless Representation for XML Documents},
  author = {Dengping Zhu and Hongwei Xi},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2895&spage=89},
  tags = {XML, XML Schema},
  researchr = {https://researchr.org/publication/ZhuX03},
  cites = {0},
  citedby = {0},
  pages = {89-104},
  booktitle = {Programming Languages and Systems, First Asian Symposium, APLAS 2003, Beijing, China, November 27-29, 2003, Proceedings},
  editor = {Atsushi Ohori},
  volume = {2895},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-20536-5},
}

@article{StumpX07,
  title = {Preface},
  author = {Aaron Stump and Hongwei Xi},
  year = {2007},
  doi = {10.1016/j.entcs.2006.10.033},
  url = {http://dx.doi.org/10.1016/j.entcs.2006.10.033},
  researchr = {https://researchr.org/publication/StumpX07},
  cites = {0},
  citedby = {0},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {174},
  number = {7},
  pages = {1-2},
}

@inproceedings{XiCC03,
  title = {Guarded recursive datatype constructors},
  author = {Hongwei Xi and Chiyan Chen and Gang Chen},
  year = {2003},
  doi = {10.1145/640128.604150},
  url = {http://doi.acm.org/10.1145/640128.604150},
  researchr = {https://researchr.org/publication/XiCC03},
  cites = {0},
  citedby = {0},
  pages = {224-235},
  booktitle = {POPL},
}

@article{AndrewsBPBIX04,
  title = {ETPS: A System to Help Students Write Formal Proofs},
  author = {Peter B. Andrews and Chad E. Brown and Frank Pfenning and Matthew Bishop and Sunil Issar and Hongwei Xi},
  year = {2004},
  doi = {10.1023/B:JARS.0000021871.18776.94},
  url = {http://dx.doi.org/10.1023/B:JARS.0000021871.18776.94},
  researchr = {https://researchr.org/publication/AndrewsBPBIX04},
  cites = {0},
  citedby = {0},
  journal = {Journal of Automated Reasoning},
  volume = {32},
  number = {1},
  pages = {75-92},
}

@inproceedings{Xi99,
  title = {Dead Code Elimination through Dependent Types},
  author = {Hongwei Xi},
  year = {1999},
  url = {http://link.springer.de/link/service/series/0558/bibs/1551/15510228.htm},
  researchr = {https://researchr.org/publication/Xi99},
  cites = {0},
  citedby = {0},
  pages = {228-242},
  booktitle = {Practical Aspects of Declarative Languages, First International Workshop, PADL  99, San Antonio, Texas, USA, January 18-19, 1999, Proceedings},
  editor = {Gopal Gupta},
  volume = {1551},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {3-540-65527-1},
}
@proceedings{plpv:2007,
  title = {Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007},
  year = {2007},
  tags = {programming languages, program verification, programming},
  researchr = {https://researchr.org/publication/plpv%3A2007},
  cites = {0},
  citedby = {0},
  booktitle = {Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007},
  conference = {plpv},
  editor = {Aaron Stump and Hongwei Xi},
  publisher = {ACM},
  isbn = {978-1-59593-677-6},
}