publications:
- title: "Eliminating Array Bound Checking Through Dependent Types"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  year: "1998"
  tags:
  - "type checking"
  researchr: "https://researchr.org/publication/XiP98"
  cites: 0
  citedby: 0
  pages: "249-257"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "XiP98"
- title: "Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell"
  author:
  - name: "Chiyan Chen"
    link: "https://researchr.org/alias/chiyan-chen"
  - name: "Dengping Zhu"
    link: "https://researchr.org/alias/dengping-zhu"
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2004"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3057&spage=239"
  links:
    doi: "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: "PADL"
  kind: "inproceedings"
  key: "ChenZX04"
- title: "Dependent Types for Program Termination Verification"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2002"
  tags:
  - "program verification"
  - "termination"
  researchr: "https://researchr.org/publication/Xi02"
  cites: 0
  citedby: 0
  journal: "lisp"
  volume: "15"
  number: "1"
  pages: "91-131"
  kind: "article"
  key: "Xi02"
- title: "Distributed meta-programming"
  author:
  - name: "Rui Shi"
    link: "https://researchr.org/alias/rui-shi"
  - name: "Chiyan Chen"
    link: "https://researchr.org/alias/chiyan-chen"
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2006"
  doi: "http://doi.acm.org/10.1145/1173706.1173743"
  links:
    doi: "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: "GPCE"
  kind: "inproceedings"
  key: "ShiCX06"
- title: "Weak and Strong Beta Normalisations in Typed Lambda-Calculi"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "1997"
  researchr: "https://researchr.org/publication/Xi97%3A0"
  cites: 0
  citedby: 0
  pages: "390-404"
  booktitle: "tlca"
  kind: "inproceedings"
  key: "Xi97:0"
- title: "Dependent Types for Program Termination Verification"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2001"
  tags:
  - "program verification"
  - "termination"
  researchr: "https://researchr.org/publication/Xi01"
  cites: 0
  citedby: 0
  pages: "231-242"
  booktitle: "lics"
  kind: "inproceedings"
  key: "Xi01"
- title: "Unifying object-oriented programming with typed functional programming"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2002"
  doi: "http://doi.acm.org/10.1145/568173.568186"
  links:
    doi: "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: "PEPM"
  kind: "inproceedings"
  key: "Xi02:0"
- title: "Simulating eta-expansions with beta-reductions in the Second-Order Polymorphic lambda-calculus"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "1997"
  researchr: "https://researchr.org/publication/Xi97"
  cites: 0
  citedby: 0
  pages: "399-409"
  booktitle: "lfcs"
  kind: "inproceedings"
  key: "Xi97"
- title: "Towards Automated Termination Proofs through "Freezing""
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "1998"
  doi: "http://link.springer.de/link/service/series/0558/bibs/1379/13790271.htm"
  links:
    doi: "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: "RTA"
  kind: "inproceedings"
  key: "Xi98"
- title: "Upper Bounds for Standardizations and An Application"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "1999"
  researchr: "https://researchr.org/publication/Xi99%3A0"
  cites: 0
  citedby: 0
  journal: "JSYML"
  volume: "64"
  number: "1"
  pages: "291-303"
  kind: "article"
  key: "Xi99:0"
- title: "Combining programming with theorem proving"
  author:
  - name: "Chiyan Chen"
    link: "https://researchr.org/alias/chiyan-chen"
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2005"
  doi: "http://doi.acm.org/10.1145/1086365.1086375"
  links:
    doi: "http://doi.acm.org/10.1145/1086365.1086375"
  tags:
  - "programming"
  researchr: "https://researchr.org/publication/ChenX05"
  cites: 0
  citedby: 0
  pages: "66-77"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "ChenX05"
- title: "Combining higher-order abstract syntax with first-order abstract syntax in ATS"
  author:
  - name: "Kevin Donnelly"
    link: "https://researchr.org/alias/kevin-donnelly"
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2005"
  doi: "http://doi.acm.org/10.1145/1088454.1088462"
  links:
    doi: "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: "ICFP"
  kind: "inproceedings"
  key: "DonnellyX05"
- title: "Facilitating Program Verification with Dependent Types"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2003"
  doi: "http://csdl.computer.org/comp/proceedings/sefm/2003/1949/00/19490072abs.htm"
  links:
    doi: "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: "SEFM"
  kind: "inproceedings"
  key: "Xi03:0"
- title: "Meta-programming through typeful code representation"
  author:
  - name: "Chiyan Chen"
    link: "https://researchr.org/alias/chiyan-chen"
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/944705.944730"
  links:
    doi: "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: "ICFP"
  kind: "inproceedings"
  key: "ChenX03"
- title: "Meta-programming through typeful code representation"
  author:
  - name: "Chiyan Chen"
    link: "https://researchr.org/alias/chiyan-chen"
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2005"
  doi: "http://dx.doi.org/10.1017/S0956796805005617"
  links:
    doi: "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: "JFP"
  volume: "15"
  number: "5"
  pages: "797-835"
  kind: "article"
  key: "ChenX05:0"
- title: "Attributive Types for Proof Erasure"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2007"
  doi: "http://dx.doi.org/10.1007/978-3-540-68103-8_13"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "Xi07:1"
- title: "TPS: A Theorem-Proving System for Classical Type Theory"
  author:
  - name: "Peter B. Andrews"
    link: "https://researchr.org/alias/peter-b.-andrews"
  - name: "Matthew Bishop"
    link: "https://researchr.org/alias/matthew-bishop"
  - name: "Sunil Issar"
    link: "https://researchr.org/alias/sunil-issar"
  - name: "Dan Nesmith"
    link: "https://researchr.org/alias/dan-nesmith"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "1996"
  tags:
  - "type system"
  - "type theory"
  researchr: "https://researchr.org/publication/AndrewsBINPX96"
  cites: 0
  citedby: 0
  journal: "JAR"
  volume: "16"
  number: "3"
  pages: "321-353"
  kind: "article"
  key: "AndrewsBINPX96"
- title: "Dependent Types in Practical Programming"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  year: "1999"
  doi: "http://doi.acm.org/10.1145/292540.292560"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "XiP99"
- title: "Safe Programming with Pointers Through Stateful Views"
  author:
  - name: "Dengping Zhu"
    link: "https://researchr.org/alias/dengping-zhu"
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2005"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3350&spage=83"
  links:
    doi: "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: "PADL"
  kind: "inproceedings"
  key: "ZhuX05"
- title: "Evaluation Under Lambda Abstraction"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "1997"
  tags:
  - "abstraction"
  researchr: "https://researchr.org/publication/Xi97%3A2"
  cites: 0
  citedby: 0
  pages: "259-273"
  booktitle: "plilp"
  kind: "inproceedings"
  key: "Xi97:2"
- title: "Perpetual Reductions in Lambda-Calculus"
  author:
  - name: "Femke van Raamsdonk"
    link: "https://researchr.org/alias/femke-van-raamsdonk"
  - name: "Paula Severi"
    link: "https://researchr.org/alias/paula-severi"
  - name: "Morten Heine Sørensen"
    link: "https://researchr.org/alias/morten-heine-s%C3%B8rensen"
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "1999"
  researchr: "https://researchr.org/publication/RaamsdonkSSX99"
  cites: 0
  citedby: 0
  journal: "iandc"
  volume: "149"
  number: "2"
  pages: "173-225"
  kind: "article"
  key: "RaamsdonkSSX99"
- title: "Towards array bound check elimination in Java :::TM::: virtual machine language"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  - name: "Songtao Xia"
    link: "https://researchr.org/alias/songtao-xia"
  year: "1999"
  doi: "http://doi.acm.org/10.1145/781995.782009"
  links:
    doi: "http://doi.acm.org/10.1145/781995.782009"
  tags:
  - "Java"
  researchr: "https://researchr.org/publication/XiX99"
  cites: 0
  citedby: 0
  pages: "14"
  booktitle: "cascon"
  kind: "inproceedings"
  key: "XiX99"
- title: "Generating Heap-Bounded Programs in a Functional Setting"
  author:
  - name: "Walid Taha"
    link: "http://www.cs.rice.edu/~taha/"
  - name: "Stephan Ellner"
    link: "https://researchr.org/alias/stephan-ellner"
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2003"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2855&spage=340"
  links:
    doi: "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: "emsoft"
  kind: "inproceedings"
  key: "TahaEX03"
- title: "Development Separation in Lambda-Calculus"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2006"
  doi: "http://dx.doi.org/10.1016/j.entcs.2005.07.014"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2005.07.014"
  researchr: "https://researchr.org/publication/Xi06"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "143"
  pages: "207-221"
  kind: "article"
  key: "Xi06"
- title: "Upper Bounds for Standardizations and an Application"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "1997"
  researchr: "https://researchr.org/publication/Xi97%3A1"
  cites: 0
  citedby: 0
  pages: "335-348"
  booktitle: "kgc"
  kind: "inproceedings"
  key: "Xi97:1"
- title: "Applied Type System: Extended Abstract"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2003"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3085&spage=394"
  links:
    doi: "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"
  kind: "inproceedings"
  key: "Xi03"
- title: "TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory"
  author:
  - name: "Peter B. Andrews"
    link: "https://researchr.org/alias/peter-b.-andrews"
  - name: "Matthew Bishop"
    link: "https://researchr.org/alias/matthew-bishop"
  - name: "Sunil Issar"
    link: "https://researchr.org/alias/sunil-issar"
  - name: "Dan Nesmith"
    link: "https://researchr.org/alias/dan-nesmith"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "1993"
  tags:
  - "type theory"
  researchr: "https://researchr.org/publication/AndrewsBINPX93"
  cites: 0
  citedby: 0
  pages: "366-370"
  booktitle: "tphol"
  kind: "inproceedings"
  key: "AndrewsBINPX93"
- title: "A Dependently Typed Assembly Language"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2001"
  researchr: "https://researchr.org/publication/XiH01"
  cites: 0
  citedby: 0
  pages: "169-180"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "XiH01"
- title: "A Typeful and Tagless Representation for XML Documents"
  author:
  - name: "Dengping Zhu"
    link: "https://researchr.org/alias/dengping-zhu"
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2003"
  doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2895&spage=89"
  links:
    doi: "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: "aplas"
  kind: "inproceedings"
  key: "ZhuX03"
- title: "Preface"
  author:
  - name: "Aaron Stump"
    link: "https://researchr.org/alias/aaron-stump"
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2007"
  doi: "http://dx.doi.org/10.1016/j.entcs.2006.10.033"
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2006.10.033"
  researchr: "https://researchr.org/publication/StumpX07"
  cites: 0
  citedby: 0
  journal: "ENTCS"
  volume: "174"
  number: "7"
  pages: "1-2"
  kind: "article"
  key: "StumpX07"
- title: "Guarded recursive datatype constructors"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  - name: "Chiyan Chen"
    link: "https://researchr.org/alias/chiyan-chen"
  - name: "Gang Chen"
    link: "https://researchr.org/alias/gang-chen"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/640128.604150"
  links:
    doi: "http://doi.acm.org/10.1145/640128.604150"
  researchr: "https://researchr.org/publication/XiCC03"
  cites: 0
  citedby: 0
  pages: "224-235"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "XiCC03"
- title: "ETPS: A System to Help Students Write Formal Proofs"
  author:
  - name: "Peter B. Andrews"
    link: "https://researchr.org/alias/peter-b.-andrews"
  - name: "Chad E. Brown"
    link: "https://researchr.org/alias/chad-e.-brown"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  - name: "Matthew Bishop"
    link: "https://researchr.org/alias/matthew-bishop"
  - name: "Sunil Issar"
    link: "https://researchr.org/alias/sunil-issar"
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "2004"
  doi: "http://dx.doi.org/10.1023/B:JARS.0000021871.18776.94"
  links:
    doi: "http://dx.doi.org/10.1023/B:JARS.0000021871.18776.94"
  researchr: "https://researchr.org/publication/AndrewsBPBIX04"
  cites: 0
  citedby: 0
  journal: "JAR"
  volume: "32"
  number: "1"
  pages: "75-92"
  kind: "article"
  key: "AndrewsBPBIX04"
- title: "Dead Code Elimination through Dependent Types"
  author:
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  year: "1999"
  doi: "http://link.springer.de/link/service/series/0558/bibs/1551/15510228.htm"
  links:
    doi: "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: "PADL"
  kind: "inproceedings"
  key: "Xi99"
- 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:
  - name: "Aaron Stump"
    link: "https://researchr.org/alias/aaron-stump"
  - name: "Hongwei Xi"
    link: "http://www.cs.bu.edu/~hwxi/"
  publisher: "ACM"
  isbn: "978-1-59593-677-6"
  kind: "proceedings"
  key: "plpv:2007"