The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Publications

Last modified: Mon Dec 1 18:35:35 2014 GMT.

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

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 (to appear), 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 (to appear), 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.

VeriML: A Dependently-Typed, User-Extensible, and Language-Centric Approach to Proof Assistant. Antonis Stampoulis, Ph.D. dissertation, Department of Computer Science, Yale University, October 2012.

Certifying Virtual Memory Manager Using Multiple Abstraction Levels. Alexander Vaynberg, Ph.D. dissertation, Department of Computer Science, Yale University, October 2012.

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.

Memory Consistency and Program Verification. Rodrigo Ferreira, Ph.D. dissertation, Department of Computer Science, Yale University, April 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.

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



Copyright © 1996-2014 The FLINT Group <flint at cs dot yale dot edu>
Yale University Department of Computer Science
Validate this page
colophon