A type system for certified binaries

ABSTRACT

A certified binary is a value together with a proof that the value satisfies a given specification. Existing compilers that generate certified code have focused on simple memory and control-flow safety rather than more advanced properties. In this paper, we present a general framework for explicitly representing complex propositions and proofs in typed intermediate and assembly languages. The new framework allows us to reason about certified programs that involve effects while still maintaining decidable typechecking. We show how to integrate an entire proof system (the calculus of inductive constructions) into a compiler intermediate language and how the intermediate language can undergo complex transformations (CPS and closure conversion) while preserving proofs represented in the type system. Our work provides a foundation for the process of automatically generating certified binaries in a typetheoretic framework.

REFERENCES

• 1: T. Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, UK, 1993.
• 2: A. W. Appel and E. W. Felten. Models for security policies in proofcarrying code. Technical Report CS-TR-636-01, Princeton Univ., Dept. of Computer Science, March 2001.
• 3: Andrew W. Appel , Amy P. Felty, A semantic model of types and machine instructions for proof-carrying code, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.243-253, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325727]
• 4: H. P. Barendregt, Lambda calculi with types, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
• 5: Henk Barendregt , Herman Geuvers, Proof-assistants using dependent type systems, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
• 6: Gilles Barthe , John Hatcliff , Morten Heine B. Sørensen, CPS Translations and Applications: The Cube and Beyond, Higher-Order and Symbolic Computation, v.12 n.2, p.125-170, September 1999 [doi>10.1023/A:1010000206149]
• 7: R. Burstall and J. McKinna. Deliverables: an approach to program development in constructions. Technical Report ECS-LFCS-91-133, Univ. of Edinburgh, UK, 1991.
• 8: Iliano Cervesato , Frank Pfenning, A Linear Logical Framework, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.264, July 27-30, 1996
• 9: Christopher Colby , Peter Lee , George C. Necula , Fred Blau , Mark Plesko , Kenneth Cline, A certifying compiler for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.95-107, June 18-21, 2000, Vancouver, British Columbia, Canada
• 10: R. Constable. Constructive mathematics as a programming logic I: Some principles of theory. Ann. of Discrete Mathemathics, 24, 1985.
• 11: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 12: K. Crary and J. Vanderwaart. An expressive, scalable type theory for certified code. Technical Report CMU-CS-01-113, School of Computer Science, Carnegie Mellon Univ., Pittsburg, PA, May 2001.
• 13: Karl Crary , David Walker , Greg Morrisett, Typed memory management in a calculus of capabilities, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.262-275, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292564]
• 14: Karl Crary , Stephanie Weirich, Flexible type analysis, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.233-248, September 27-29, 1999, Paris, France
• 15: Karl Crary , Stephnie Weirich, Resource bound certification, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.184-198, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325716]
• 16: Karl Crary , Stephanie Weirich , Greg Morrisett, Intensional polymorphism in type-erasure semantics, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.301-312, September 26-29, 1998, Baltimore, Maryland, United States
• 17: H. Geuvers. Logics and Type Systems. PhD thesis, Catholic University of Nijmegen, The Netherlands, 1993.
• 18: J.-Y. Girard. Interpretation Fonctionnelle et Elimination des Coupures dans l'Arithmetique d'Ordre Superieur. PhD thesis, University of Paris VII, 1972.
• 19: R. Harper. The practice of type theory. Talk presented at 2000 Alan J. Perlis Symposium, Yale University, New Haven, CT, April 2000.
• 20: Robert Harper , Mark Lillibridge, Explicit polymorphism and CPS conversion, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.206-219, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158630]
• 21: Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
• 22: Susumu Hayashi, Singleton, Union and Intersection Types for Program Extraction, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.701-730, September 24-27, 1991
• 23: W. A. Howard. The formulae-as-types notion of constructions. In To H.B.Curry: Essays on Computational Logic, Lambda Calculus and Formalism. Academic Press, 1980.
• 24: G. Huet, C. Paulin-Mohring, et al. The Coq proof assistant reference manual. Part of the Coq system version 6.3.1, May 2000.
• 25: Yasuhiko Minamide , Greg Morrisett , Robert Harper, Typed closure conversion, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.271-283, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237791]
• 26: Stefan Monnier , Bratin Saha , Zhong Shao, Principled scavenging, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.81-91, June 2001, Snowbird, Utah, United States
• 27: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-97, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268954]
• 28: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 29: George Ciprian Necula , Peter Lee, Compiling with proofs, 1998
• 30: George C. Necula , Peter Lee, Safe kernel extensions without run-time checking, Proceedings of the second USENIX symposium on Operating systems design and implementation, p.229-243, October 29-November 01, 1996, Seattle, Washington, United States
• 31: George C. Necula , Peter Lee, The design and implementation of a certifying compiler, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.333-344, June 17-19, 1998, Montreal, Quebec, Canada
• 32: Bengt Nordström , Kent Petersson , Jan M. Smith, Programming in Martin-Lo¨f's type theory: an introduction, Clarendon Press, New York, NY, 1990
• 33: C. Paulin-Mohring, Extracting &ohgr;'s programs from proofs in the calculus of constructions, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.89-104, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75285]
• 34: Christine Paulin-Mohring, Inductive Definitions in the system Coq - Rules and Properties, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.328-345, March 16-18, 1993
• 35: Z. Shao. An overview of the FLINT/ML compiler. In Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation, June 1997.
• 36: Zhong Shao , Christopher League , Stefan Monnier, Implementing typed intermediate languages, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.313-323, September 26-29, 1998, Baltimore, Maryland, United States
• 37: Z. Shao, B. Saha, V. Trifonov, and N. Papaspyrou. A type system for certified binaries. Technical Report YALEU/DCS/TR-1211, Dept. of Computer Science, Yale University, New Haven, CT, March 2001.
• 38: Mark A. Sheldon , David K. Gifford, Static dependent types for first class modules, Proceedings of the 1990 ACM conference on LISP and functional programming, p.20-29, June 27-29, 1990, Nice, France [doi>10.1145/91556.91577]
• 39: Valery Trifonov , Bratin Saha , Zhong Shao, Fully reflexive intensional type analysis, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.82-93, September 2000
• 40: David Walker, A type system for expressive security policies, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.254-267, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325728]
• 41: B. Werner. Une Theoriedes Constructions Inductives. PhD thesis, A L'Universite Paris 7, Paris, France, 1994.
• 42: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]
• 43: Hongwei Xi , Robert Harper, A dependently typed assembly language, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
• 44: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]