Research

People

Publications

Software

Support

Links

Internal

Publications

Last modified: Tue Jun 10 19:09:26 2008 GMT.

Listed in reverse chronological order. This BibTeX file contains entries for some publications listed on this page.

The Mechanized Verification of Garbage Collector Implementations. Andrew McCreight, Ph.D. dissertation, Department of Computer Science, Yale University, December 2008.

Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. Xinyu Feng, Zhong Shao, Yuan Dong and Yu Guo. In Proc. 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08), Tucson, Arizona, pages 170-182, June 2008. ©2008 ACM.

An Open Framework for Certified System Software. Xinyu Feng, Ph.D. dissertation, Department of Computer Science, Yale University, December 2007.

Using XCAP to Certify Realistic System Code: Machine Context Management. Zhaozhong Ni, Dachuan Yu, and Zhong Shao. In Proc. 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'07), Kaiserslautern, Germany, September 2007. Lecture Notes in Computer Science Vol. 4732, pages 189-206. © 2007 Springer-Verlag.

Certified Self-Modifying Code. Hongxu Cai, Zhong Shao, and Alexander Vaynberg. In Proc. 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'07), San Diego, CA, pages 66-77, June 2007. ©2007 ACM.

A General Framework for Certifying Garbage Collectors and Their Mutators. Andrew McCreight, Zhong Shao, Chunxiao Lin, and Long Li. In Proc. 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'07), San Diego, CA, pages 468-479, June 2007. ©2007 ACM.

Foundational Typed Assembly Language with Certified Garbage Collection. Chunxiao Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, and Yu Guo. In Proc. 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE'07), Shanghai, China, pages 326-335, June 2007. ©2007 IEEE Computer Society.

On the Relationship between Concurrent Separation Logic and Assume-Guarantee Reasoning Xinyu Feng, Rodrigo Ferreira, and Zhong Shao. In Proc. 16th European Symposium on Programming (ESOP'07), Braga, Portugal, March 2007. Lecture Notes in Computer Science Vol. 4421, pages 173-188. © 2007 Springer-Verlag.

An Open Framework for Foundational Proof-Carrying Code. Xinyu Feng, Zhaozhong Ni, Zhong Shao, and Yu Guo. In Proc. 2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI'07), Nice, France, pages 67-78, January 2007. ©2007 ACM.

Modular Machine Code Verification. Zhaozhong Ni, Ph.D. dissertation, Department of Computer Science, Yale University, November 2006.

Modular Verification of Assembly Code with Stack-Based Control Abstractions. Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, and Zhaozhong Ni. In Proc. 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'06), Ottawa, Canada, pages 401-414, June 2006. ©2006 ACM.

Certified Assembly Programming with Embedded Code Pointers. Zhaozhong Ni and Zhong Shao. In Proc. 33rd ACM Symposium on Principles of Programming Languages (POPL'06), Charleston, South Carolina, pages 320-333, January 2006. ©2006 ACM.

Modular Verification of Concurrent Assembly Code with Dynamic Thread Creation and Termination. Xinyu Feng and Zhong Shao. In Proc. 2005 ACM SIGPLAN International Conference on Functional Programming (ICFP'05), Tallinn, Estonia, pages 254-267, September 2005. ©2005 ACM.

A Type System for Certified Binaries. Zhong Shao, Valery Trifonov, Bratin Saha, and Nikolaos Papaspyrou. In ACM Transactions on Programming Languages and Systems (TOPLAS), 27(1), pages 1-45, January 2005. ©2005 ACM.

Verification of Safety Properties for Concurrent Assembly Code. Dachuan Yu and Zhong Shao. In Proc. 2004 ACM SIGPLAN International Conference on Functional Programming (ICFP'04), Snowbird, Utah, pages 175-188, September 2004. ©2004 ACM.

Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code. Nadeem A. Hamid and Zhong Shao. In Proc. 17th International Conference on the Applications of Higher Order Logic Theorem Proving (TPHOLs'04), Park City, Utah, September 2004. Lecture Notes in Computer Science Vol. 3223, pages 118-135. © 2004 Springer-Verlag.

Building Certified Libraries for PCC: Dynamic Storage Allocation (Extended Version). Dachuan Yu, Nadeem A. Hamid, and Zhong Shao. In Science of Computer Programming (Special Issue ESOP 2003), 50 (1-3): 101-127, March 2004. ©2004 Elsevier.

A Syntactic Approach to Foundational Proof-Carrying Code (Extended Version). Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, and Zhaozhong Ni. Journal of Automated Reasoning (Special Issue on Proof-Carrying Code) 31 (3-4): 191-229, 2003.

Building Certified Libraries for PCC: Dynamic Storage Allocation. Dachuan Yu, Nadeem A. Hamid, and Zhong Shao. In Proc. 2003 European Symposium on Programming (ESOP'03), Warsaw, Poland, April 2003. Lecture Notes in Computer Science Vol. 2618. © Springer-Verlag. (Also available as Technical Report YALEU/DCS/TR-1247, Department of Computer Science, Yale University, January 2003).

Precision in Practice: A Type-Preserving Java Compiler. Christopher League, Zhong Shao, and Valery Trifonov. In Proc. 12th International Conference on Compiler Construction (CC'03), Warsaw, Poland, April 2003. Lecture Notes in Computer Science Vol. 2622. © Springer-Verlag.

Typed Regions. Stefan Monnier and Zhong Shao. Technical Report YALEU/DCS/TR-1242, Department of Computer Science, Yale University, October 2002.

Intensional Analysis of Higher-Kinded Recursive Types. Gregory D. Collins and Zhong Shao. Technical Report YALEU/DCS/TR-1240, Department of Computer Science, Yale University, October 2002.

A Type-Preserving Compiler Infrastructure. Christopher League, Ph.D. dissertation.

A Type System For Certified Runtime Type Analysis. Bratin Saha, Ph.D. dissertation.

Intensional Analysis of Quantified Types. Bratin Saha, Valery Trifonov, and Zhong Shao. In ACM Transactions on Programming Languages and Systems (TOPLAS), 25(2), pages 159-209, March 2003. ©2003 ACM.

Supporting Binary Compatibility with Static Compilation. Dachuan Yu, Zhong Shao, and Valery Trifonov. In USENIX 2nd Java[TM] Virtual Machine Research and Technology Symposium (JVM'02), San Francisco, California, pages 165-180, August 2002. Winner of the Best Student Paper Award. ©2002 USENIX.

A Syntactic Approach to Foundational Proof-Carrying Code. Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, and Zhaozhong Ni. In Proc. 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), Copenhagen, Denmark, pages 89-100, July 2002. ©2007 IEEE Computer Society.

Type-Preserving Compilation of Featherweight IL. Dachuan Yu, Valery Trifonov, Zhong Shao. In Proc. 2002 Workshop on Formal Techniques for Java-like Programs (FTfJP'02), Malaga, Spain, June 2002. (Also available as Technical Report YALEU/DCS/TR-1228, Department of Computer Science, Yale University, April 2002).

Type-Preserving Compilation of Featherweight Java. Christopher League, Zhong Shao, and Valery Trifonov. In ACM Transactions on Programming Languages and Systems (TOPLAS), 24(2), pages 112-152, March 2002. ©2002 ACM.

A Type System for Certified Binaries. Zhong Shao, Bratin Saha, Valery Trifonov, and Nikolaos Papaspyrou. In Proc. 29th ACM Symposium on Principles of Programming Languages (POPL'02), Portland, OR, pages 217-232, January 2002, ©2002 ACM.

A Type System for Certified Binaries (Extended Version). Zhong Shao, Bratin Saha, Valery Trifonov, and Nikolaos Papaspyrou. Technical Report YALEU/DCS/TR-1211, Department of Computer Science, Yale University, March 2001 (revised September 2001).

Inlining as Staged Computation. Stefan Monnier and Zhong Shao. In Journal of Functional Programming, 13(3), pages 647-676, May 2003. ©2003 Cambridge University Press.

Functional Java Bytecode. Christopher League, Valery Trifonov, and Zhong Shao. In Proc. 2001 Workshop on Intermediate Representation Engineering for the Java Virtual Machine at the 5th World Multi-conference on Systemics, Cybernetics, and Informatics, Orlando, FL, July 2001.

Principled Scavenging. Stefan Monnier, Bratin Saha, and Zhong Shao. In Proc. 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'01), Snowbird, UT, pages 81-91, June 2001. ©2001 ACM.

Type-Based Certifying Compilation. Zhong Shao. Invited tutorial given at the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'01), Snowbird, UT, June 2001. ©2001 ACM.

An Encoding of Fomega in LF. Carsten Schürmann, Dachuan Yu, and Zhaozhong Ni. In Proc. 2001 Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN'01), Siena, Italy, June 2001.

Type-Preserving Compilation of Featherweight Java. Christopher League, Valery Trifonov, and Zhong Shao. 8th Foundations of Object-Oriented Languages Workshop (FOOL'8). London, January 2001

Fully Reflexive Intensional Type Analysis in Type Erasure Semantics. Bratin Saha, Valery Trifonov, and Zhong Shao. In Third ACM SIGPLAN Workshop on Types in Compilation (TIC'00), Montreal, Canada, September 2000. (Also available as Technical Report YALEU/DCS/TR-1197, Department of Computer Science, Yale University, June 2000).

Fully Reflexive Intensional Type Analysis. Valery Trifonov, Bratin Saha, and Zhong Shao. In Proc. 2000 ACM SIGPLAN International Conference on Functional Programming (ICFP'00), Montreal, Canada, pages 82-93, September 2000. ©2000 ACM.

Fully Reflexive Intensional Type Analysis (Extended Version). Bratin Saha, Valery Trifonov, and Zhong Shao. Technical Report YALEU/DCS/TR-1194, Department of Computer Science, Yale University, March 2000.

Algorithm-Independent Framework for Verifying Integer Constraints. David Teller and Zhong Shao. Technical Report YALEU/DCS/TR-1195, Department of Computer Science, Yale University, March 2000.

Efficient and Safe-for-Space Closure Conversion. Zhong Shao and Andrew W. Appel. In ACM Transactions on Programming Languages and Systems (TOPLAS), 22(1), pages 129-161, January 2000. ©2000 ACM.

Representing Java Classes in a Typed Intermediate Language. Christopher League, Zhong Shao, and Valery Trifonov. In Proc. 1999 ACM SIGPLAN International Conference on Functional Programming (ICFP'99), Paris, France, pages 183-196, September 1999. ©1999 ACM.

Transparent Modules with Fully Syntactic Signatures. Zhong Shao. In Proc. 1999 ACM SIGPLAN International Conference on Functional Programming (ICFP'99), Paris, France, pages 220-232, September 1999. ©1999 ACM.

Transparent Modules with Fully Syntactic Signatures (Extended Version). Zhong Shao. Technical Report YALEU/DCS/TR-1181 (supersedes TR 1161), Department of Computer Science, Yale University, June 1999.

Principles and a Preliminary Design for ML2000. The ML2000 Working Group. March 1999.

Safe and Principled Language Interoperation. Valery Trifonov and Zhong Shao. In Proc. 1999 European Symposium on Programming (ESOP'99), Amsterdam, The Netherlands, March 1999. Lecture Notes in Computer Science, Springer-Verlag.

Scaling Proof-Carrying Code to Production Compilers and Security Policies. Andrew W. Appel, Edward W. Felton and Zhong Shao. Technical Report YALEU/DCS/TR-1182, Department of Computer Science, Yale University, January 1999.

SubTransitive CFA Using Types . Bratin Saha, Nevin Heintze, and Dino Oliva. Technical Report YALEU/DCS/TR-1166, Department of Computer Science, Yale University, October 1998.

Implementing Typed Intermediate Languages. Zhong Shao, Christopher League, and Stefan Monnier. In Proc. 1998 ACM SIGPLAN International Conference on Functional Programming (ICFP'98), Baltimore, Maryland, pages 313-323, September 1998. ©1998 ACM.

Typed Cross-Module Compilation. Zhong Shao. In Proc. 1998 ACM SIGPLAN International Conference on Functional Programming (ICFP'98), Baltimore, Maryland, pages 141-152, September 1998. ©1998 ACM.

Typed Cross-Module Compilation (Extended Version). Zhong Shao. Technical Report YALEU/DCS/TR-1126, Department of Computer Science, Yale University, June 1998.

Formal Semantics of the FLINT Intermediate Language. Christopher League and Zhong Shao. Technical Report 1171, May 1998.

Type-Directed Continuation Allocation. Zhong Shao and Valery Trifonov. In Proc. Second International Workshop on Types in Compilation (TIC'98), pages 116-135, Kyoto, Japan, March 1998. Lecture Notes in Computer Science Vol 1473, Springer-Verlag.

Optimal Type Lifting. Bratin Saha and Zhong Shao. In the Second International Workshop on Types in Compilation (TIC'98), Kyoto, Japan, pages 156-177, March 1998. Lecture Notes in Computer Science Vol 1473, Springer-Verlag.

Optimal Type Lifting (Extended Version). Bratin Saha and Zhong Shao. Technical Report YALEU/DCS/TR-1159, Department of Computer Science, Yale University, August 1998.

Typed Common Intermediate Format. Zhong Shao. In 1997 USENIX Conference on Domain-Specific Languages, Santa Barbara, California, October 1997.

Flexible Representation Analysis. Zhong Shao. In Proc. 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP'97), Amsterdam, The Netherlands, pages 85-98, June 1997. ©1997 ACM. [TR version available]

An Overview of the FLINT/ML Compiler. Zhong Shao. In Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation (TIC'97). Amsterdam, The Netherlands, June 1997.

Empirical and Analytic Study of Stack vs. Heap Cost for Languages with Closures. Andrew W. Appel and Zhong Shao. In Journal of Functional Programming, 6(1): 47-74, January 1996. ©1996 Cambridge University Press.

A Type-Based Compiler for Standard ML. Zhong Shao and Andrew W. Appel. In Proc. 1995 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'95), La Jolla, CA, pages 116-129, June 1995. ©1995 ACM.

Compiling Standard ML for Efficient Execution on Modern Machines. Zhong Shao. Ph.D. Thesis. Dept. of Computer Science, Princeton University, November 1994.

Space-Efficient Closure Representations. Zhong Shao and Andrew W. Appel. In Proc. 1994 ACM Conference on Lisp and Functional Programming (LFP'94), Orlando, FL, page 150-161, June 1994. ©1994 ACM.

Unrolling Lists. Zhong Shao, John H. Reppy, and Andrew W. Appel. In Proc. 1994 ACM Conference on Lisp and Functional Programming (LFP'94), Orlando, FL, page 185-195, June 1994. ©1994 ACM.

Inferring Type Maps during Garbage Collection. Hans Boehm and Zhong Shao. In Proc. OOPSLA'93 Workshop on Memory Management and Garbage Collection, Washington, DC, September 1993.

Smartest Recompilation. Zhong Shao and Andrew W. Appel. In Proc. Twentieth ACM Symposium on Principles of Programming Languages (POPL'93), Charleston, SC, page 439-450, January 1993. ©1993 ACM. [TR version available]

Callee-Save Registers in Continuation-Passing Style. Andrew W. Appel and Zhong Shao. In Lisp and Symbolic Computation, 5(3), page 189-219, 1992.