Type-Based Certifying Compilation

PLDI'01 Tutorial Accompanying References

I. Introduction and Motivation

• George Necula. Proof-carrying code. In Conference Record of POPL '97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106--119, Paris, France, 15--17 January 1997.

• George Necula and Peter Lee. Safe kernel extensions without run-time checking. In Proceedings of the Second Symposium on Operating Systems Design and Implementation, pages 229--243, Seattle, WA, October 1996.

• Andrew Appel. Foundational proof-carrying code. In Proceedings of 16th Annual IEEE Symposium on Logic in Computer Science (LICS'01), pages 247--258, June 2001.

• Andrew Appel, Ed Felten, and Zhong Shao. Scaling proof-carrying code to production compilers and security policies. Technical Report YALEU/DCS/TR-1182, Department of Computer Science, Yale University, January 1999.

II. A Hacker's Guide to Type Theory

• Henk Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T.S.E. Maibaum (Ed.): Handbook of Logic in Computer Science, Volume 2 Background: Computational Structures. Oxford Science Publications, 1992.

• Henk Barendregt and Herman Geuvers. Proof-assistants using dependent type systems. In A. Robinson and A. Voronkov (Ed.): Handbook of Automated Reasoning. Elservier Science Publishers, 2001.

• Luca Cardelli. Type systems. In Allen B. Tucker (Ed.): The Computer Science and Engineering Handbook. CRC Press, 1997, ISBN: 0-8493-2909-4. Chapter 103, pp 2208-2236.

• Karl Crary and Greg Morrisett. Type structure for low-level programming languages. In 1999 International Colloquium on Automata, Languages, and Programming, 1999.

• Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. In Conference Record of POPL '98: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 85--97, January 1998.

• Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based typed assembly language. In 1998 Workshop on Types in Compilation, Kyoto, Japan, March 1998.

III. Certifying Low-Level Features

• Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Conference Record of POPL '99: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 262--275, January 1999.

• Karl Crary and Stephanie Weirich. Flexible type analysis. In Proceedings of the Fourth International Conference on Functional Programming (ICFP '99), pages 233--248, Paris, France, September 1999.

• Karl Crary and Stephanie Weirich. Resource bound certification. In Conference Record of POPL '00: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 184--198, January 2000.

• Robert Harper and Greg Morrisett. Compiling polymorphism using intensional type analysis. In 21nd Annual ACM Symp. on Principles of Prog. Languages, Pages 130-141, January, 1995.

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

• Valery Trifonov, Bratin Saha, and Zhong Shao. Fully reflexive intensional type analysis. In Proc. ACM SIGPLAN International Conference on Functional Programming (ICFP'00), pages 82-93, September 2000.

• Daniel Wang and Andrew Appel. Type-preserving garbage collectors. In 28th Annual ACM Symp. on Principles of Prog. Languages, pages 166-178, January, 2001.

• Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In 26th Annual ACM Symp. on Principles of Prog. Languages (POPL'99), pages 214-227, January, 1999.

• Hongwei Xi and Robert Harper. A dependently typed assembly language. In Proc. ACM SIGPLAN International Conference on Functional Programming (ICFP'01), pages (to appear), September 2001.

IV. Certifying High-Level Features

• R. Harper, J. Mitchell, and E. Moggi. Higher-order modules and the phase distinction. In 17th Annual ACM Symp. on Principles of Prog. Languages (POPL'90), pages 341-354, January, 1990.

• Christopher League, Zhong Shao, and Valery Trifonov. Representing Java classes in a typed intermediate language. In Proc. ACM SIGPLAN International Conference on Functional Programming (ICFP'99), pages 183--196, September 1999.

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

• Zhong Shao. Typed cross-module compilation. In Proc. ACM SIGPLAN International Conference on Functional Programming (ICFP'98), September 1998.

• Zhong Shao. Transparent modules with fully syntactic Signatures. In Proc. ACM SIGPLAN International Conference on Functional Programming (ICFP'99), pages 220--232, September 1999.

V. Engineering Type-Based Compilers

• Bratin Saha and Zhong Shao. Optimal type lifting. In Proc. 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.

• Zhong Shao, Christopher League, and Stefan Monnier. Implementing typed intermediate languages. In Proc. ACM SIGPLAN International Conference on Functional Programming (ICFP'98), September 1998.

• Dan Grossman and Greg Morrisett. Scalable certification for typed assembly language. In the 2000 ACM SIGPLAN Workshop on Types in Compilation, Montreal, Canada, September 2000.

• George C. Necula and Peter Lee. The design and implementation of a certifying compiler. In Proceedings of the ACM SIGPLAN'98 Conference on Programming Language Design and Implementation (PLDI), pages 333--344, Montreal, Canada, 17--19 June 1998.