 | 2009 |
|---|
| 49 |       | Zhong Shao,
Benjamin C. Pierce:
Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009
ACM 2009 |
| 48 |  | Gang Tan,
Zhong Shao,
Xinyu Feng,
Hongxu Cai:
Weak updates and separation logic.
APLAS 2009: 178-193 |
| 47 | | Zhong Shao:
Modular Development of Certified System Software.
TASE 2009: 5 |
| 46 | | Xinyu Feng,
Zhong Shao,
Yu Guo,
Yuan Dong:
Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads.
J. Autom. Reasoning 42(2-4): 301-347 (2009) |
| 2008 |
|---|
| 45 | | Xinyu Feng,
Zhong Shao,
Yuan Dong,
Yu Guo:
Certifying low-level programs with hardware interrupts and preemptive threads.
PLDI 2008: 170-182 |
| 44 | | Xinyu Feng,
Zhong Shao,
Yu Guo,
Yuan Dong:
Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems.
VSTTE 2008: 54-69 |
| 2007 |
|---|
| 43 | | Zhong Shao:
Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, Singapore, November 29-December 1, 2007, Proceedings
Springer 2007 |
| 42 | | Xinyu Feng,
Rodrigo Ferreira,
Zhong Shao:
On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning.
ESOP 2007: 173-188 |
| 41 | | Andrew McCreight,
Zhong Shao,
Chunxiao Lin,
Long Li:
A general framework for certifying garbage collectors and their mutators.
PLDI 2007: 468-479 |
| 40 | | Hongxu Cai,
Zhong Shao,
Alexander Vaynberg:
Certified self-modifying code.
PLDI 2007: 66-77 |
| 39 | | Chunxiao Lin,
Andrew McCreight,
Zhong Shao,
Yiyun Chen,
Yu Guo:
Foundational Typed Assembly Language with Certified Garbage Collection.
TASE 2007: 326-338 |
| 38 | | Xinyu Feng,
Zhaozhong Ni,
Zhong Shao,
Yu Guo:
An open framework for foundational proof-carrying code.
TLDI 2007: 67-78 |
| 37 | | Zhaozhong Ni,
Dachuan Yu,
Zhong Shao:
Using XCAP to Certify Realistic Systems Code: Machine Context Management.
TPHOLs 2007: 189-206 |
| 2006 |
|---|
| 36 | | Xinyu Feng,
Zhong Shao,
Alexander Vaynberg,
Sen Xiang,
Zhaozhong Ni:
Modular verification of assembly code with stack-based control abstractions.
PLDI 2006: 401-414 |
| 35 | | Zhaozhong Ni,
Zhong Shao:
Certified assembly programming with embedded code pointers.
POPL 2006: 320-333 |
| 2005 |
|---|
| 34 | | Xinyu Feng,
Zhong Shao:
Modular verification of concurrent assembly code with dynamic thread creation and termination.
ICFP 2005: 254-267 |
| 33 | | Zhong Shao,
Valery Trifonov,
Bratin Saha,
Nikolaos Papaspyrou:
A type system for certified binaries.
ACM Trans. Program. Lang. Syst. 27(1): 1-45 (2005) |
| 2004 |
|---|
| 32 | | Dachuan Yu,
Zhong Shao:
Verification of safety properties for concurrent assembly code.
ICFP 2004: 175-188 |
| 31 | | Nadeem Abdul Hamid,
Zhong Shao:
Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code.
TPHOLs 2004: 118-135 |
| 30 | | Dachuan Yu,
Nadeem Abdul Hamid,
Zhong Shao:
Building certified libraries for PCC: dynamic storage allocation.
Sci. Comput. Program. 50(1-3): 101-127 (2004) |
| 2003 |
|---|
| 29 | | Zhong Shao,
Peter Lee:
Proceedings of TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, New Orleans, Louisiana, USA, January 18, 2003
ACM 2003 |
| 28 | | Christopher League,
Zhong Shao,
Valery Trifonov:
Precision in Practice: A Type-Preserving Java Compiler.
CC 2003: 106-120 |
| 27 | | Dachuan Yu,
Nadeem Abdul Hamid,
Zhong Shao:
Building Certified Libraries for PCC: Dynamic Storage Allocation.
ESOP 2003: 363-379 |
| 26 | | Bratin Saha,
Valery Trifonov,
Zhong Shao:
Intensional analysis of quantified types.
ACM Trans. Program. Lang. Syst. 25(2): 159-209 (2003) |
| 25 | | Nadeem Abdul Hamid,
Zhong Shao,
Valery Trifonov,
Stefan Monnier,
Zhaozhong Ni:
A Syntactic Approach to Foundational Proof-Carrying Code.
J. Autom. Reasoning 31(3-4): 191-229 (2003) |
| 24 | | Stefan Monnier,
Zhong Shao:
Inlining as staged computation.
J. Funct. Program. 13(3): 647-676 (2003) |
| 2002 |
|---|
| 23 | | Dachuan Yu,
Zhong Shao,
Valery Trifonov:
Supporting Binary Compatibility with Static Compilation.
Java™ Virtual Machine Research and Technology Symposium 2002: 165-180 |
| 22 | | Nadeem Abdul Hamid,
Zhong Shao,
Valery Trifonov,
Stefan Monnier,
Zhaozhong Ni:
A Syntactic Approach to Foundational Proof-Carrying Code.
LICS 2002: 89-100 |
| 21 | | Zhong Shao,
Bratin Saha,
Valery Trifonov,
Nikolaos Papaspyrou:
A type system for certified binaries.
POPL 2002: 217-232 |
| 20 | | Christopher League,
Zhong Shao,
Valery Trifonov:
Type-preserving compilation of Featherweight Java.
ACM Trans. Program. Lang. Syst. 24(2): 112-152 (2002) |
| 2001 |
|---|
| 19 | | Stefan Monnier,
Bratin Saha,
Zhong Shao:
Principled Scavenging.
PLDI 2001: 81-91 |
| 18 | | Zhong Shao:
Invited Talk: Towards a Principled Multi-Language Infrastructure.
Electr. Notes Theor. Comput. Sci. 59(1): (2001) |
| 2000 |
|---|
| 17 | | Valery Trifonov,
Bratin Saha,
Zhong Shao:
Fully reflexive intensional type analysis.
ICFP 2000: 82-93 |
| 16 | | Zhong Shao,
Andrew W. Appel:
Efficient and safe-for-space closure conversion.
ACM Trans. Program. Lang. Syst. 22(1): 129-161 (2000) |
| 1999 |
|---|
| 15 | | Valery Trifonov,
Zhong Shao:
Safe and Principled Language Interoperation.
ESOP 1999: 128-146 |
| 14 | | Christopher League,
Zhong Shao,
Valery Trifonov:
Representing Java Classes in a Typed Intermediate Language.
ICFP 1999: 183-196 |
| 13 | | Zhong Shao:
Transparent Modules with Fully Syntactic Signatures.
ICFP 1999: 220-232 |
| 1998 |
|---|
| 12 | | Zhong Shao:
Typed Cross-Module Compilation.
ICFP 1998: 141-152 |
| 11 | | Zhong Shao,
Christopher League,
Stefan Monnier:
Implementing Typed Intermediate Languages.
ICFP 1998: 313-323 |
| 10 | | Zhong Shao,
Valery Trifonov:
Type-Directed Continuation Allocation.
Types in Compilation 1998: 116-135 |
| 9 | | Bratin Saha,
Zhong Shao:
Optimal Type Lifting.
Types in Compilation 1998: 156-177 |
| 1997 |
|---|
| 8 | | Zhong Shao:
Typed Common Intermediate Format.
DSL 1997: 89-102 |
| 7 | | Zhong Shao:
Flexible Representation Analysis.
ICFP 1997: 85-98 |
| 1996 |
|---|
| 6 | | Andrew W. Appel,
Zhong Shao:
Empirical and Analytic Study of Stack Versus Heap Cost for Languages with Closures.
J. Funct. Program. 6(1): 47-74 (1996) |
| 1995 |
|---|
| 5 | | Zhong Shao,
Andrew W. Appel:
A Type-Based Compiler for Standard ML.
PLDI 1995: 116-129 |
| 1994 |
|---|
| 4 | | Zhong Shao,
Andrew W. Appel:
Space-Efficient Closure Representations.
LISP and Functional Programming 1994: 150-161 |
| 3 | | Zhong Shao,
John H. Reppy,
Andrew W. Appel:
Unrolling Lists.
LISP and Functional Programming 1994: 185-195 |
| 1993 |
|---|
| 2 | | Zhong Shao,
Andrew W. Appel:
Smartest Recompilation.
POPL 1993: 439-450 |
| 1992 |
|---|
| 1 | | Andrew W. Appel,
Zhong Shao:
Callee-Save Registers in Continuation-Passing Style.
Lisp and Symbolic Computation 5(3): 191-221 (1992) |
