Zhong Shao - researchr alias

researchr

You are not signed in
Sign in
Sign up

2011

Weak Updates and Separation LogicGang Tan, Zhong Shao, Xinyu Feng, Hongxu Cai. ngc, 29(1):3-29, 2011. [doi]

2010

2009

2008

Certifying low-level programs with hardware interrupts and preemptive threadsXinyu Feng, Zhong Shao, Yuan Dong, Yu Guo. PLDI 2008: 170-182 [doi]

Combining Domain-Specific and Foundational Logics to Verify Complete Software SystemsXinyu Feng, Zhong Shao, Yu Guo, Yuan Dong. vstte 2008: 54-69 [doi]

2007

Certified self-modifying codeHongxu Cai, Zhong Shao, Alexander Vaynberg. PLDI 2007: 66-77 [doi]

On the Relationship Between Concurrent Separation Logic and Assume-Guarantee ReasoningXinyu Feng, Rodrigo Ferreira, Zhong Shao. ESOP 2007: 173-188 [doi]

An open framework for foundational proof-carrying codeXinyu Feng, Zhaozhong Ni, Zhong Shao, Yu Guo. tldi 2007: 67-78 [doi]

Foundational Typed Assembly Language with Certified Garbage CollectionChunxiao Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, Yu Guo. tase 2007: 326-338 [doi]

A general framework for certifying garbage collectors and their mutatorsAndrew McCreight, Zhong Shao, Chunxiao Lin, Long Li. PLDI 2007: 468-479 [doi]

Using XCAP to Certify Realistic Systems Code: Machine Context ManagementZhaozhong Ni, Dachuan Yu, Zhong Shao. tphol 2007: 189-206 [doi]

Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, Singapore, November 29-December 1, 2007, ProceedingsZhong Shao, editor, Volume 4807 of Lecture Notes in Computer Science, Springer, 2007.

2006

Modular verification of assembly code with stack-based control abstractionsXinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, Zhaozhong Ni. PLDI 2006: 401-414 [doi]

Certified assembly programming with embedded code pointersZhaozhong Ni, Zhong Shao. POPL 2006: 320-333 [doi]

2005

Modular verification of concurrent assembly code with dynamic thread creation and terminationXinyu Feng, Zhong Shao. ICFP 2005: 254-267 [doi]

A type system for certified binariesZhong Shao, Valery Trifonov, Bratin Saha, Nikolaos Papaspyrou. TOPLAS, 27(1):1-45, 2005. [doi]

2004

Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying CodeNadeem Abdul Hamid, Zhong Shao. tphol 2004: 118-135 [doi]

Building certified libraries for PCC: dynamic storage allocationDachuan Yu, Nadeem Abdul Hamid, Zhong Shao. SCP, 50(1-3):101-127, 2004. [doi]

Verification of safety properties for concurrent assembly codeDachuan Yu, Zhong Shao. ICFP 2004: 175-188 [doi]

2003

A Syntactic Approach to Foundational Proof-Carrying CodeNadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni. JAR, 31(3-4):191-229, 2003. [doi]

Precision in Practice: A Type-Preserving Java CompilerChristopher League, Zhong Shao, Valery Trifonov. cc 2003: 106-120 [doi]

Inlining as staged computationStefan Monnier, Zhong Shao. JFP, 13(3):647-676, 2003. [doi]

Intensional analysis of quantified typesBratin Saha, Valery Trifonov, Zhong Shao. TOPLAS, 25(2):159-209, 2003. [doi]

Proceedings of TLDI 03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, New Orleans, Louisiana, USA, January 18, 2003Zhong Shao, Peter Lee, editors, ACM, 2003.

Building Certified Libraries for PCC: Dynamic Storage AllocationDachuan Yu, Nadeem Abdul Hamid, Zhong Shao. ESOP 2003: 363-379 [doi]

2002

2001

Principled ScavengingStefan Monnier, Bratin Saha, Zhong Shao. PLDI 2001: 81-91

Invited Talk: Towards a Principled Multi-Language InfrastructureZhong Shao. TCS, 59(1), 2001. [doi]

2000

Efficient and safe-for-space closure conversionZhong Shao, Andrew W. Appel. TOPLAS, 22(1):129-161, 2000. [doi]

Fully reflexive intensional type analysisValery Trifonov, Bratin Saha, Zhong Shao. ICFP 2000: 82-93 [doi]

1999

Representing Java Classes in a Typed Intermediate LanguageChristopher League, Zhong Shao, Valery Trifonov. ICFP 1999: 183-196 [doi]

Transparent Modules with Fully Syntactic SignaturesZhong Shao. ICFP 1999: 220-232 [doi]

Safe and Principled Language InteroperationValery Trifonov, Zhong Shao. ESOP 1999: 128-146 [doi]

1998

1997

Typed Common Intermediate FormatZhong Shao. DSL 1997: 89-102 [doi]

Flexible Representation AnalysisZhong Shao. ICFP 1997: 85-98

1996

Empirical and Analytic Study of Stack Versus Heap Cost for Languages with ClosuresAndrew W. Appel, Zhong Shao. JFP, 6(1):47-74, 1996.

1995

A Type-Based Compiler for Standard MLZhong Shao, Andrew W. Appel. PLDI 1995: 116-129

1994

Unrolling ListsZhong Shao, John H. Reppy, Andrew W. Appel. lfp 1994: 185-195 [doi]

Space-Efficient Closure RepresentationsZhong Shao, Andrew W. Appel. lfp 1994: 150-161 [doi]

1993

Smartest RecompilationZhong Shao, Andrew W. Appel. POPL 1993: 439-450

1992

Callee-Save Registers in Continuation-Passing StyleAndrew W. Appel, Zhong Shao. lisp, 5(3):191-221, 1992.