2009 |
46 | | 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 |
2008 |
45 | EE | Xinyu Feng,
Zhong Shao,
Yuan Dong,
Yu Guo:
Certifying low-level programs with hardware interrupts and preemptive threads.
PLDI 2008: 170-182 |
44 | EE | 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 | EE | Xinyu Feng,
Rodrigo Ferreira,
Zhong Shao:
On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning.
ESOP 2007: 173-188 |
41 | EE | Andrew McCreight,
Zhong Shao,
Chunxiao Lin,
Long Li:
A general framework for certifying garbage collectors and their mutators.
PLDI 2007: 468-479 |
40 | EE | Hongxu Cai,
Zhong Shao,
Alexander Vaynberg:
Certified self-modifying code.
PLDI 2007: 66-77 |
39 | EE | Chunxiao Lin,
Andrew McCreight,
Zhong Shao,
Yiyun Chen,
Yu Guo:
Foundational Typed Assembly Language with Certified Garbage Collection.
TASE 2007: 326-338 |
38 | EE | Xinyu Feng,
Zhaozhong Ni,
Zhong Shao,
Yu Guo:
An open framework for foundational proof-carrying code.
TLDI 2007: 67-78 |
37 | EE | Zhaozhong Ni,
Dachuan Yu,
Zhong Shao:
Using XCAP to Certify Realistic Systems Code: Machine Context Management.
TPHOLs 2007: 189-206 |
2006 |
36 | EE | 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 | EE | Zhaozhong Ni,
Zhong Shao:
Certified assembly programming with embedded code pointers.
POPL 2006: 320-333 |
2005 |
34 | EE | Xinyu Feng,
Zhong Shao:
Modular verification of concurrent assembly code with dynamic thread creation and termination.
ICFP 2005: 254-267 |
33 | EE | 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 | EE | Dachuan Yu,
Zhong Shao:
Verification of safety properties for concurrent assembly code.
ICFP 2004: 175-188 |
31 | EE | Nadeem Abdul Hamid,
Zhong Shao:
Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code.
TPHOLs 2004: 118-135 |
30 | EE | 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 | EE | Christopher League,
Zhong Shao,
Valery Trifonov:
Precision in Practice: A Type-Preserving Java Compiler.
CC 2003: 106-120 |
27 | EE | Dachuan Yu,
Nadeem Abdul Hamid,
Zhong Shao:
Building Certified Libraries for PCC: Dynamic Storage Allocation.
ESOP 2003: 363-379 |
26 | EE | Bratin Saha,
Valery Trifonov,
Zhong Shao:
Intensional analysis of quantified types.
ACM Trans. Program. Lang. Syst. 25(2): 159-209 (2003) |
25 | EE | 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 | EE | Stefan Monnier,
Zhong Shao:
Inlining as staged computation.
J. Funct. Program. 13(3): 647-676 (2003) |
2002 |
23 | EE | Dachuan Yu,
Zhong Shao,
Valery Trifonov:
Supporting Binary Compatibility with Static Compilation.
Java Virtual Machine Research and Technology Symposium 2002: 165-180 |
22 | EE | Nadeem Abdul Hamid,
Zhong Shao,
Valery Trifonov,
Stefan Monnier,
Zhaozhong Ni:
A Syntactic Approach to Foundational Proof-Carrying Code.
LICS 2002: 89-100 |
21 | EE | Zhong Shao,
Bratin Saha,
Valery Trifonov,
Nikolaos Papaspyrou:
A type system for certified binaries.
POPL 2002: 217-232 |
20 | EE | 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 | EE | Zhong Shao:
Invited Talk: Towards a Principled Multi-Language Infrastructure.
Electr. Notes Theor. Comput. Sci. 59(1): (2001) |
2000 |
17 | EE | Valery Trifonov,
Bratin Saha,
Zhong Shao:
Fully reflexive intensional type analysis.
ICFP 2000: 82-93 |
16 | EE | Zhong Shao,
Andrew W. Appel:
Efficient and safe-for-space closure conversion.
ACM Trans. Program. Lang. Syst. 22(1): 129-161 (2000) |
1999 |
15 | EE | Valery Trifonov,
Zhong Shao:
Safe and Principled Language Interoperation.
ESOP 1999: 128-146 |
14 | EE | Christopher League,
Zhong Shao,
Valery Trifonov:
Representing Java Classes in a Typed Intermediate Language.
ICFP 1999: 183-196 |
13 | EE | Zhong Shao:
Transparent Modules with Fully Syntactic Signatures.
ICFP 1999: 220-232 |
1998 |
12 | EE | Zhong Shao:
Typed Cross-Module Compilation.
ICFP 1998: 141-152 |
11 | EE | Zhong Shao,
Christopher League,
Stefan Monnier:
Implementing Typed Intermediate Languages.
ICFP 1998: 313-323 |
10 | EE | Zhong Shao,
Valery Trifonov:
Type-Directed Continuation Allocation.
Types in Compilation 1998: 116-135 |
9 | EE | Bratin Saha,
Zhong Shao:
Optimal Type Lifting.
Types in Compilation 1998: 156-177 |
1997 |
8 | EE | 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 | EE | Zhong Shao,
Andrew W. Appel:
Space-Efficient Closure Representations.
LISP and Functional Programming 1994: 150-161 |
3 | EE | 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) |