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

Compositionality and Observational Refinement for Linearizability with Crashes. Arthur Oliveira Vale, Zhongye Wang, Yixuan Chen, Peixin You, and Zhong Shao. In Proceedings of the ACM on Programming Languages (PACMPL), Volume 8, Number OOPSLA2, Article 352 (October 2024), 29 pages.

LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs. Longfei Qiu, Yoonseung Kim, Ji-Yoon Shin, Jieung Kim, Wolf Honore, and Zhong Shao. In Proceedings of the ACM on Programming Languages (PACMPL), Volume 8, Number PLDI, Article 193 (June 2024), 25 pages.

A Compositional Theory of Linearizability (Extended Version). Arthur Oliveira Vale, Zhong Shao, and Yixuan Chen. In Journal of the ACM, Volume 71, Number 2, Article 14 (April 2024), 107 pages.

AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects. Wolf Honore, Longfei Qiu, Yoonseung Kim, Ji-Yoon Shin, Jieung Kim, and Zhong Shao. In Proceedings of the ACM on Programming Languages (PACMPL), Volume 8, Number OOPSLA1, Article 109 (April 2024), 30 pages.

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. Ling Zhang, Yuting Wang, Jinhua Wu, Jeremie Koenig, and Zhong Shao. In Proceedings of the ACM on Programming Languages (PACMPL), Volume 8, Number POPL, Article 72 (January 2024), 31 pages.

Ou: Automating the Parallelization of Zero-Knowledge Protocols. Yuyang Sang, Ning Luo, Samuel Judson, Ben Chaimberg, Timos Antonopoulos, Xiao Wang, Ruzica Piskac, and Zhong Shao. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS'23), Copenhagen, Denmark, pages 534-548, November 2023.

A Compositional Theory of Linearizability. Arthur Oliveira Vale, Zhong Shao, and Yixuan Chen. In Proceedings of the ACM on Programming Languages (PACMPL), Volume 7, Number POPL, Article 38 (January 2023), 32 pages.

Compositional Virtual Timeline: Verifying Dynamic-Priority Partitions with Algorithmic Temporal Isolation. Mengqi Liu, Zhong Shao, Hao Chen, Man-Ki Yoon, and Jung-Eun Kim. In Proceedings of the ACM on Programming Languages (PACMPL), Volume 6, Number OOPSLA2, Article 127 (October 2022), 29 pages.

Adore: Atomic Distributed Objects with Certified Reconfiguration. Wolf Honore, Ji-Yong Shin, Jieung Kim, and Zhong Shao. In Proc. 2022 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'22), San Diego, California, USA, 16 pages, June 2022.

Layered and Object-Based Game Semantics. Arthur Oliveira Vale, Paul-Andre Mellies, Zhong Shao, Jeremie Koenig, and Leo Stefanesco. In Proceedings of the ACM on Programming Languages (PACMPL), Volume 6, Number POPL, Article 42 (January 2022), 32 pages.

Verified Compilation of C Programs with a Nominal Memory Model. Yuting Wang, Ling Zhang, Zhong Shao, and Jeremie Koenig. In Proceedings of the ACM on Programming Languages (PACMPL), Volume 6, Number POPL, Article 25 (January 2022), 31 pages.

Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems. Wolf Honore, Jieung Kim, Ji-Yong Shin, and Zhong Shao. In Proceedings of the ACM on Programming Languages (PACMPL), Volume 5, Number OOPSLA, Article 97 (October 2021), 31 pages.

Blinder: Partition-Oblivious Hierarchical Scheduling. Man-Ki Yoon, Mengqi Liu, Hao Chen, Jung-Eun Kim, and Zhong Shao. In Proc. 30th USENIX Security Symposium on (USENIX Security 2021), August 2021.

CompCertO: Compiling Certified Open C Components. Jérémie Koenig and Zhong Shao. In Proc. 2021 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'21), Virtual, Canada, 15 pages, June 2021.

CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files. Yuting Wang, Xiangzhe Xu, Pierre Wilke, and Zhong Shao. In Proceedings of the ACM on Programming Languages (PACMPL), Volume 4, Number OOPSLA, Article 197 (November 2020), 28 pages.

Refinement-Based Game Semantics for Certified Abstraction Layers. Jérémie Koenig and Zhong Shao. In Proc. 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'20), Saarbrücken, Germany, pages 633-647, July 2020.

Task-Aware Novelty Detection for Visual-Based Deep Learning in Autonomous Systems. Valerie Chen, Man-Ki Yoon, and Zhong Shao. In Proc. 2020 IEEE International Conference on Robotics and Automation (ICRA'20), Paris, France, pages 11060-11066, June 2020.

ABC: Abstract prediction Before Concreteness. Jung-Eun Kim, Richard Bradford, Man-Ki Yoon, and Zhong Shao. In Proc. 2020 Design, Automation, & Test in Europe Conference & Exhibition (DATE'20), Grenoble, France, May 2020.

AnytimeNet: Controlling Time-Quality TradeOffs in Deep Neural Network Architectures. Jung-Eun Kim, Richard Bradford, and Zhong Shao. In Proc. 2020 Design, Automation, & Test in Europe Conference & Exhibition (DATE'20), Grenoble, France, May 2020.

Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation. Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, and Man-Ki Yoon. In Proceedings of the ACM on Programming Languages (PACMPL), Volume 4, Number POPL, Article 20 (January 2020), 31 pages.

WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems. Ji-Yong Shin, Jieung Kim, Wolf Honore, Hernán Vanzetto, Srihari Radhakrishnan, Mahesh Balakrishnan, and Zhong Shao. In Proc. 2019 ACM Symposium on Cloud Computing (SOCC'19), Santa Cruz, California. Pages 299-311, November 2019.

Building Certified Concurrent OS Kernels. Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, Jérémie Koenig, Newman Wu, Vilhelm Sjöberg, and David Costanzo. In Communications of the ACM, 62(10), pages 89-99, October 2019.

DeepSEA: A Language for Certified System Software. Vilhelm Sjöberg, Yuyang Sang, Shu-Chun Weng, and Zhong Shao. In Proceedings of the ACM on Programming Languages (PACMPL), Volume 3, Number OOPSLA, Article 136 (October 2019), 27 pages.

Integrating Formal Schedulability Analysis into a Verified OS Kernel. Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, and Zhong Shao. In Proc. 31st International Conference on Computer Aided Verification (CAV 2019), New York, USA Part II, LNCS 11562, pages 496-514, July 2019.

ADLP: Accountable Data Logging Protocol for Publish-Subscribe Communication Systems. Man-Ki Yoon and Zhong Shao. In Proc. 2019 IEEE 39th International Conference on Distributed Computing Systems (ICDCS'19), Dallas, Texas. Pages 1149-1160, July 2019.

An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code. Yuting Wang, Pierre Wilke, and Zhong Shao. In Proceedings of the ACM on Programming Languages (PACMPL), Volume 3, Number POPL, Article 62 (January 2019), 30 pages.

Certified Concurrent Abstraction Layers. Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, and Tahina Ramananandro. In Proc. 2018 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'18), Philadelphia, PA, pages 646-661, June 2018.

Safety and Liveness of MCS Lock---Layer by Layer, Jieung Kim, Vilhelm Sjöberg, Ronghui Gu, and Zhong Shao. In Proc. 15th Asian Symposium on Programming Languages and Systems (APLAS'17), Suzhou, China, November 2017. Lecture Notes in Computer Science Vol. 10695, pages 273-297. © 2017 Springer-Verlag.

Position Paper: The Science of Deep Specification, Andrew Appel, Lennart Beringer, Adam Chlipala, Benjamin Pierce, Zhong Shao, Stephanie Weirich, and Steve Zdancewic. In Philosophical Transactions of the Royal Society A, Volume 375, issue 2104, 24 pages, October 2017.

Automated Resource Analysis with Coq Proof Objects. Quentin Carbonneaux, Jan Hoffmann, Thomas Reps, and Zhong Shao. In Proc. 29th International Conference on Computer Aided Verification (CAV 2017), Heidelberg, Germany, Part II, pages 64-85, July 2017.

CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. In Proc. 2016 USENIX Symposium on Operating Systems Design and Implementation (OSDI'16), Savannah, GA, pages 653-669, November 2016.

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers. Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, and Ronghui Gu. In Proc. 2016 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'16), Santa Barbara, CA, pages 431-447, June 2016. An extended version of this paper appeared in Journal of Automated Reasoning (JAR), volume 61, issue 1-4, pages 141-189, June 2018.

End-to-End Verification of Information-Flow Security for C and Assembly Programs. David Costanzo, Zhong Shao, and Ronghui Gu. In Proc. 2016 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'16), Santa Barbara, CA, pages 648-664, June 2016.

Compositional Certified Resource Bounds. Quentin Carbonneaux, Jan Hoffmann, and Zhong Shao. In Proc. 2015 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15), Portland, OR, pages 467-478, June 2015.

Automatic Static Cost Analysis for Parallel Programs. Jan Hoffmann and Zhong Shao. In Proc. 24th European Symposium on Programming (ESOP'15), London, UK, April 2015. Lecture Notes in Computer Science, Vol. 9032, pages 132-157.

Deep Specifications and Certified Abstraction Layers. Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. In Proc. 42nd ACM Symposium on Principles of Programming Languages (POPL'15), Mumbia, India, pages 595-608, January 2015.

A Compositional Semantics for Verified Separate Compilation and Linking. Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, and Yuchen Fu. In Proc. 4th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP'15), Mumbia, India, pages 3-14, January 2015.

Compositional Verification of Termination-Preserving Refinement of Concurrent Programs. Hongjin Liang, Xinyu Feng, and Zhong Shao. In Proc. 23rd EACSL Annual Conference on Computer Science Logic and 29th Annual IEEE Symposium on Logic in Computer Science (CSL-LICS'14), Vienna, Austria, Paper No. 65, July 2014. ©2014 IEEE Computer Society.

End-to-End Verification of Stack-Space Bounds for C Programs. Quentin Carbonneaux, Jan Hoffmann, Tahina Ramananandro, and Zhong Shao. In Proc. 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'14), Edinburgh, UK pages 270-281, June 2014. ©2014 ACM.

Type-Based Amortized Resource Analysis with Integers and Arrays, Jan Hoffmann and Zhong Shao In Proc. 12th International Symposium on Functional and Logic Programming (FLOPS'14), Kanazawa, Japan, June 2014. Lecture Notes in Computer Science, Vol. 8475, pages 152-168. © 2014 Springer-Verlag.

A Separation Logic for Enforcing Declarative Information Flow Control Policies, David Costanzo and Zhong Shao In Proc. 3rd Conference on Principles of Security and Trust (POST'14), Grenoble, France, April 2014. Lecture Notes in Computer Science, Vol. 8414, pages 179-198. © 2014 Springer-Verlag.

Characterizing Progress Properties of Concurrent Objects via Contextual Refinements, Hongjin Liang, Jan Hoffmann, Xinyu Feng, and Zhong Shao. In Proc. 24th International Conference on Concurrency Theory (CONCUR'13), Buenos Aires, Argentina, August 2013. Lecture Notes in Computer Science Vol. 8052, pages 227-241. © 2013 Springer-Verlag.

Quantitative Reasoning for Proving Lock-Freedom. Jan Hoffmann, Michael Marmar, and Zhong Shao. In Proc. 28th Annual IEEE Symposium on Logic in Computer Science (LICS'13), New Orleans, USA, pages 124-133, June 2013. ©2013 IEEE Computer Society.

Compositional Verification of a Baby Virtual Memory Manager, Alexander Vaynberg and Zhong Shao. In Proc. 2nd International Conference on Certified Programs and Proofs (CPP'12), Kyoto, Japan, December 2012. Lecture Notes in Computer Science Vol. 7679, pages 143-159. © 2012 Springer-Verlag.

A Case for Behavior-Preserving Actions in Separation Logic, David Costanzo and Zhong Shao. In Proc. 10th Asian Symposium on Programming Languages and Systems (APLAS'12), Kyoto, Japan, December 2012. Lecture Notes in Computer Science Vol. 7705, pages 332-349. © 2012 Springer-Verlag.

Modular Verification of Concurrent Thread Management, Yu Guo, Xinyu Feng, Zhong Shao, and Peizhi Shi. In Proc. 10th Asian Symposium on Programming Languages and Systems (APLAS'12), Kyoto, Japan, December 2012. Lecture Notes in Computer Science Vol. 7705, pages 315-331. © 2012 Springer-Verlag.

Static and User-Extensible Proof Checking. Antonis Stampoulis and Zhong Shao. In Proc. 39th ACM Symposium on Principles of Programming Languages (POPL'12), Philadelphia, Pennsylvania, pages 273-284, January 2012. ©2012 ACM.

A Simple Model for Certifying Assembly Programs with First-Class Function Pointers. Wei Wang, Zhong Shao, Xinyu Jiang, and Yu Guo. In Proc. 4th IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE'11), Xian, China, pages 125-132, August 2011. ©2011 IEEE Computer Society.

CertiKOS: A Certified Kernel for Secure Cloud Computing. Liang Gu, Alexander Vaynberg, Bryan Ford, Zhong Shao, and David Costanzo. In Proc. 2nd ACM SIGOPS Asia-Pacific Workshop on Systems (APSys'11), Shanghai, China, July 2011. ©2011 ACM.

Certifying the Concurrent State Table Implementation in a Surgical Robotic System (Extended Version). Yanni Kouskoulas, Ming Fu, Zhong Shao, and Peter Kazanzides. A shorter summary of this paper appeared in Proc. 3rd Joint Workshop on High Confidence Medical Devices, Software, and Systems & Medical Device Plug-and-Play Interoperability, Chicago, USA. June 2011.

Weak Updates and Separation Logic. Gang Tan, Zhong Shao, Xinyu Feng, and Hongxu Cai. In New Generation Computing: Computing Paradigms and Computational Intelligence, Volume 29, No. 1, 2011, pages 1-29. © Ohmsha, Ltd. and Springer 2011. An earlier version appeared in Proc. 7th Asian Symposium on Programming Languages and Systems (APLAS'09), Seoul, Korea, December 2009. Lecture Notes in Computer Science Vol. 5904, pages 178-193.

Certified Software, Zhong Shao. In Communications of the ACM, 53(12), pages 56-66, December 2010. ©2010 ACM.

VeriML: Typed Computation of Logical Terms inside a Language with Effects, Antonis Stampoulis and Zhong Shao. In Proc. 2010 ACM SIGPLAN International Conference on Functional Programming (ICFP'10), Baltimore, Maryland, pages 333-344, September 2010. ©2010 ACM.

Reasoning about Optimistic Concurrency Using a Program Logic for History, Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, and Yu Zhang. In Proc. 21st International Conference on Concurrency Theory (CONCUR'10), Paris, France, August 2010. Lecture Notes in Computer Science Vol. 6269, pages 388-402. © 2010 Springer-Verlag.

Advanced Development of Certified OS Kernels. Zhong Shao and Bryan Ford. Technical Report YALEU/DCS/TR-1436, Department of Computer Science, Yale University, July 2010.

Parametrized Memory Models and Concurrent Separation Logic, Rodrigo Ferreira, Xinyu Feng, and Zhong Shao. In Proc. 19th European Symposium on Programming (ESOP'10), Paphos, Cyprus, March 2010. Lecture Notes in Computer Science Vol. 6012, pages 267-286. © 2010 Springer-Verlag.

Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads (Extended Version). Xinyu Feng, Zhong Shao, Yu Guo, and Yuan Dong. Journal of Automated Reasoning (Special Issue on Operating System Verification) 42 (2-4): 301-347, April 2009. © Springer Science + Business Media B.V.2009.

Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. Xinyu Feng, Zhong Shao, Yu Guo and Yuan Dong. In Proc. Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'08), Toronto, Canada, October 2008. Lecture Notes in Computer Science Vol. 5295, pages 54-69. © 2008 Springer-Verlag.

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.

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 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.

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.

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.

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.