| 2007 |
|---|
| 41 | | Aaron Stump,
Hongwei Xi:
Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007
ACM 2007 |
| 40 | EE | Hongwei Xi:
Attributive Types for Proof Erasure.
TYPES 2007: 188-202 |
| 39 | EE | Kevin Donnelly,
Hongwei Xi:
A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F.
Electr. Notes Theor. Comput. Sci. 174(5): 109-125 (2007) |
| 38 | EE | Aaron Stump,
Hongwei Xi:
Preface.
Electr. Notes Theor. Comput. Sci. 174(7): 1-2 (2007) |
| 37 | EE | Hongwei Xi:
Dependent ML An approach to practical programming with dependent types.
J. Funct. Program. 17(2): 215-286 (2007) |
| 2006 |
|---|
| 36 | EE | Rui Shi,
Chiyan Chen,
Hongwei Xi:
Distributed meta-programming.
GPCE 2006: 243-248 |
| 35 | EE | Hongwei Xi:
Development Separation in Lambda-Calculus.
Electr. Notes Theor. Comput. Sci. 143: 207-221 (2006) |
| 34 | EE | Chiyan Chen,
Rui Shi,
Hongwei Xi:
Implementing Typeful Program Transformations.
Fundam. Inform. 69(1-2): 103-121 (2006) |
| 2005 |
|---|
| 33 | EE | Sa Cui,
Kevin Donnelly,
Hongwei Xi:
ATS: A Language That Combines Programming with Theorem Proving.
FroCos 2005: 310-320 |
| 32 | EE | Chiyan Chen,
Hongwei Xi:
Combining programming with theorem proving.
ICFP 2005: 66-77 |
| 31 | EE | Kevin Donnelly,
Hongwei Xi:
Combining higher-order abstract syntax with first-order abstract syntax in ATS.
MERLIN 2005: 58-63 |
| 30 | EE | Dengping Zhu,
Hongwei Xi:
Safe Programming with Pointers Through Stateful Views.
PADL 2005: 83-97 |
| 29 | EE | Chiyan Chen,
Hongwei Xi:
Meta-programming through typeful code representation.
J. Funct. Program. 15(5): 797-835 (2005) |
| 2004 |
|---|
| 28 | EE | Chiyan Chen,
Rui Shi,
Hongwei Xi:
A Typeful Approach to Object-Oriented Programming with Multiple Inheritance.
PADL 2004: 23-38 |
| 27 | EE | Chiyan Chen,
Dengping Zhu,
Hongwei Xi:
Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell.
PADL 2004: 239-254 |
| 26 | EE | Peter B. Andrews,
Chad E. Brown,
Frank Pfenning,
Matthew Bishop,
Sunil Issar,
Hongwei Xi:
ETPS: A System to Help Students Write Formal Proofs.
J. Autom. Reasoning 32(1): 75-92 (2004) |
| 2003 |
|---|
| 25 | EE | Dengping Zhu,
Hongwei Xi:
A Typeful and Tagless Representation for XML Documents.
APLAS 2003: 89-104 |
| 24 | EE | Walid Taha,
Stephan Ellner,
Hongwei Xi:
Generating Heap-Bounded Programs in a Functional Setting.
EMSOFT 2003: 340-355 |
| 23 | EE | Chiyan Chen,
Hongwei Xi:
Meta-programming through typeful code representation.
ICFP 2003: 275-286 |
| 22 | EE | Chiyan Chen,
Hongwei Xi:
Implementing typeful program transformations.
PEPM 2003: 20-28 |
| 21 | EE | Hongwei Xi,
Chiyan Chen,
Gang Chen:
Guarded recursive datatype constructors.
POPL 2003: 224-235 |
| 20 | EE | Hongwei Xi:
Facilitating Program Verification with Dependent Types.
SEFM 2003: 72-81 |
| 19 | EE | Hongwei Xi:
Applied Type System: Extended Abstract.
TYPES 2003: 394-408 |
| 2002 |
|---|
| 18 | EE | Hongwei Xi:
Unifying object-oriented programming with typed functional programming.
ASIA-PEPM 2002: 117-125 |
| 17 | | Hongwei Xi:
Dependent Types for Program Termination Verification.
Higher-Order and Symbolic Computation 15(1): 91-131 (2002) |
| 2001 |
|---|
| 16 | | Hongwei Xi,
Robert Harper:
A Dependently Typed Assembly Language.
ICFP 2001: 169-180 |
| 15 | | Hongwei Xi:
Dependent Types for Program Termination Verification.
LICS 2001 |
| 2000 |
|---|
| 14 | EE | Hongwei Xi:
Imperative Programming with Dependent Types.
LICS 2000: 375-387 |
| 1999 |
|---|
| 13 | EE | Hongwei Xi,
Songtao Xia:
Towards array bound check elimination in Java TM virtual machine language.
CASCON 1999: 14 |
| 12 | EE | Hongwei Xi:
Dead Code Elimination through Dependent Types.
PADL 1999: 228-242 |
| 11 | EE | Hongwei Xi,
Frank Pfenning:
Dependent Types in Practical Programming.
POPL 1999: 214-227 |
| 10 | | Femke van Raamsdonk,
Paula Severi,
Morten Heine Sørensen,
Hongwei Xi:
Perpetual Reductions in Lambda-Calculus.
Inf. Comput. 149(2): 173-225 (1999) |
| 9 | | Hongwei Xi:
Upper Bounds for Standardizations and An Application.
J. Symb. Log. 64(1): 291-303 (1999) |
| 1998 |
|---|
| 8 | | Hongwei Xi,
Frank Pfenning:
Eliminating Array Bound Checking Through Dependent Types.
PLDI 1998: 249-257 |
| 7 | EE | Hongwei Xi:
Towards Automated Termination Proofs through "Freezing".
RTA 1998: 271-285 |
| 1997 |
|---|
| 6 | | Hongwei Xi:
Upper Bounds for Standardizations and an Application.
Kurt Gödel Colloquium 1997: 335-348 |
| 5 | | Hongwei Xi:
Simulating eta-expansions with beta-reductions in the Second-Order Polymorphic lambda-calculus.
LFCS 1997: 399-409 |
| 4 | | Hongwei Xi:
Evaluation Under Lambda Abstraction.
PLILP 1997: 259-273 |
| 3 | | Hongwei Xi:
Weak and Strong Beta Normalisations in Typed Lambda-Calculi.
TLCA 1997: 390-404 |
| 1996 |
|---|
| 2 | | Peter B. Andrews,
Matthew Bishop,
Sunil Issar,
Dan Nesmith,
Frank Pfenning,
Hongwei Xi:
TPS: A Theorem-Proving System for Classical Type Theory.
J. Autom. Reasoning 16(3): 321-353 (1996) |
| 1993 |
|---|
| 1 | | Peter B. Andrews,
Matthew Bishop,
Sunil Issar,
Dan Nesmith,
Frank Pfenning,
Hongwei Xi:
TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory.
HUG 1993: 366-370 |
