Zhong Shao
Nikolaos Papaspyrou
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.
- 1.T. Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, UK, 1993.Google Scholar
- 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.Google Scholar
- 3.A. W. Appel and A. P. Felty. A semantic model of types and machine instructions for proof-carrying code. In Proc. 27th ACM Symp. on Principles of Prog. Lang., pages 243-253. ACM Press, 2000. Google ScholarDigital Library
- 4.H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science (volume 2). Oxford Univ. Press, 1991. Google ScholarDigital Library
- 5.H. P. Barendregt and H. Geuvers. Proof-assistants using dependent type systems. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier Sci. Pub. B.V., 1999. Google ScholarDigital Library
- 6.G. Barthe, J. Hatcliff, and M. Sorensen. CPS translations and applications: the cube and beyond. Higher Order and Symbolic Computation, 12(2):125-170, September 1999. Google ScholarDigital Library
- 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.Google Scholar
- 8.I. Cervesato and F. Pfenning. A linear logical framework. In Proc. 11th IEEE Symp. on Logic in Computer Science, pages 264-275, July 1996. Google ScholarDigital Library
- 9.C. Colby, P. Lee, G. C. Necula, F. Blau, M. Plesko, and K. Cline. A certifying compiler for Java. In Proc. 2000 ACM Conf. on Prog. Lang. Design and Impl., pages 95-107, New York, 2000. ACM Press. Google ScholarDigital Library
- 10.R. Constable. Constructive mathematics as a programming logic I: Some principles of theory. Ann. of Discrete Mathemathics, 24, 1985.Google Scholar
- 11.T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95-120, 1988. Google ScholarDigital Library
- 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.Google Scholar
- 13.K. Crary, D. Walker, and G. Morrisett. Typed memory management in a calculus of capabilities. In Proc. 26th ACM Symp. on Principles of Prog. Lang., pages 262-275. ACM Press, 1999. Google ScholarDigital Library
- 14.K. Crary and S. Weirich. Flexible type analysis. In Proc. 1999 ACM SIGPLAN Int'l Conf. on Functional Prog., pages 233-248. ACM Press, Sept. 1999. Google ScholarDigital Library
- 15.K. Crary and S. Weirich. Resource bound certification. In Proc. 27th ACM Symp. on Principles of Prog. Lang., pages 184-198. ACMPress, 2000. Google ScholarDigital Library
- 16.K. Crary, S. Weirich, and G. Morrisett. Intensional polymorphism in type-erasure semantics. In Proc. 1998 ACM SIGPLAN Int'l Conf. on Functional Prog., pages 301-312. ACM Press, Sept. 1998. Google ScholarDigital Library
- 17.H. Geuvers. Logics and Type Systems. PhD thesis, Catholic University of Nijmegen, The Netherlands, 1993.Google Scholar
- 18.J.-Y. Girard. Interpretation Fonctionnelle et Elimination des Coupures dans l'Arithmetique d'Ordre Superieur. PhD thesis, University of Paris VII, 1972.Google Scholar
- 19.R. Harper. The practice of type theory. Talk presented at 2000 Alan J. Perlis Symposium, Yale University, New Haven, CT, April 2000.Google Scholar
- 20.R. Harper and M. Lillibridge. Explicit polymorphism and CPS conversion. In Proc. 20th ACM Symp. on Principles of Prog. Lang., pages 206-219. ACM Press, 1993. Google ScholarDigital Library
- 21.R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Proc. 22nd ACM Symp. on Principles of Prog. Lang., pages 130-141. ACM Press, 1995. Google ScholarDigital Library
- 22.S. Hayashi. Singleton, union and intersection types for program extraction. In A. R. Meyer, editor, Proc. International Conference on Theoretical Aspects of Computer Software, pages 701-730, 1991. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- 25.Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Proc. 23rd ACM Symp. on Principles of Prog. Lang., pages 271- 283. ACM Press, 1996. Google ScholarDigital Library
- 26.S. Monnier, B. Saha, and Z. Shao. Principled scavenging. In Proc. 2001 ACM Conf. on Prog. Lang. Design and Impl., pages 81-91, New York, 2001. ACM Press. Google ScholarDigital Library
- 27.G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. In Proc. 25th ACM Symp. on Principles of Prog. Lang., pages 85-97. ACM Press, Jan. 1998. Google ScholarDigital Library
- 28.G. Necula. Proof-carrying code. In Proc. 24th ACM Symp. on Principles of Prog. Lang., pages 106-119, New York, Jan 1997. ACM Press. Google ScholarDigital Library
- 29.G. Necula. Compiling with Proofs. PhD thesis, School of Computer Science, Carnegie Mellon Univ., Sept. 1998. Google ScholarDigital Library
- 30.G. Necula and P. Lee. Safe kernel extensions without run-time checking. In Proc. 2nd USENIX Symp. on Operating System Design and Impl., pages 229-243. USENIX Assoc., 1996. Google ScholarDigital Library
- 31.G. Necula and P. Lee. The design and implementation of a certifying compiler. In Proc. 1998 ACM Conf. on Prog. Lang. Design and Impl., pages 333-344, New York, 1998. ACM Press. Google ScholarDigital Library
- 32.B. Nordstrom, K. Petersson, and J. Smith. Programming in Martin- Lof's type theory. Oxford University Press, 1990. Google ScholarDigital Library
- 33.C. Paulin-Mohring. Extracting F 's programs from proofs in the Calculus of Constructions. In Proc. 16th ACM Symp. on Principles of Prog. Lang., pages 89-104, New York, Jan 1989. ACM Press. Google ScholarDigital Library
- 34.C. Paulin-Mohring. Inductive definitions in the system Coq-rules and properties. In M. Bezem and J. Groote, editors, Proc. TLCA. LNCS 664, Springer-Verlag, 1993. Google ScholarDigital Library
- 35.Z. Shao. An overview of the FLINT/ML compiler. In Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation, June 1997.Google Scholar
- 36.Z. Shao, C. League, and S. Monnier. Implementing typed intermediate languages. In Proc. 1998 ACMSIGPLAN Int'l Conf. on Functional Prog., pages 313-323. ACM Press, 1998. Google ScholarDigital Library
- 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.Google Scholar
- 38.M. A. Sheldon and D. K. Gifford. Static dependent types for first class modules. In 1990 ACM Conference on Lisp and Functional Programming, pages 20-29, New York, June 1990. ACM Press. Google ScholarDigital Library
- 39.V. Trifonov, B. Saha, and Z. Shao. Fully reflexive intensional type analysis. In Proc. 2000 ACM SIGPLAN Int'l Conf. on Functional Prog., pages 82-93. ACM Press, September 2000. Google ScholarDigital Library
- 40.D. Walker. A type system for expressive security policies. In Proc. 27th ACM Symp. on Principles of Prog. Lang., pages 254-267, 2000. Google ScholarDigital Library
- 41.B. Werner. Une Theoriedes Constructions Inductives. PhD thesis, A L'Universite Paris 7, Paris, France, 1994.Google Scholar
- 42.A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38-94, 1994. Google ScholarDigital Library
- 43.H. Xi and R. Harper. A dependently typed assembly language. In Proc. 2001 ACM SIGPLAN Int'l Conf. on Functional Prog., pages 169-180. ACM Press, September 2001. Google ScholarDigital Library
- 44.H. Xi and F. Pfenning. Dependent types in practical programming. In Proc. 26th ACM Symp. on Principles of Prog. Lang., pages 214-227. ACM Press, 1999. Google ScholarDigital Library
- A type system for certified binaries
Recommendations
A type system for certified binaries
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 ...
A type system for certified binaries
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,...
Comments