A certified type-preserving compiler from lambda calculus to assembly language

ABSTRACT

We present a certified compiler from the simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler and the terms of its several intermediate languages are given dependent types that guarantee that only well-typed programs are representable. Thus, type preservation for each compiler pass follows without any significant "proofs" of the usual kind. Semantics preservation is proved based on denotational semantics assigned to the intermediate languages. We demonstrate how working with a type-preserving compiler enables type-directed proof search to discharge large parts of our proof obligations automatically.

REFERENCES

• 1: Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The PoplMark challenge. In Proc. TPHOLs, pages 50--65, 2005.
• 2: Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
• 3: Samuel Boutin, Using Reflection to Build Efficient and Certified Decision Procedures, Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software, p.515-529, September 23-26, 1997
• 4: Maulik A. Dave, Compiler verification: a bibliography, ACM SIGSOFT Software Engineering Notes, v.28 n.6, November 2003 [doi>10.1145/966221.966235]
• 5: Nicolas G. de Bruijn. Lambda-calculus notation with nameless dummies: a tool for automatic formal manipulation with application to the Church--Rosser theorem. Indag. Math., 34(5):381--392, 1972.
• 6: Eduardo Giménez, Codifying Guarded Definitions with Recursive Schemes, Selected papers from the International Workshop on Types for Proofs and Programs, p.39-59, June 06-10, 1994
• 7: Joshua D. Guttman , John D. Ramsdell , Mitchell Wand, VLISP: a verified implementation of Scheme, Lisp and Symbolic Computation, v.8 n.1-2, p.5-32, March 1995 [doi>10.1007/BF01128406]
• 8: Furio Honsell , Donald Sannella, Pre-logical Relations, Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic, p.546-561, September 20-25, 1999
• 9: Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-54, January 11-13, 2006, Charleston, South Carolina, USA
• 10: Conor McBride , James McKinna, The view from the left, Journal of Functional Programming, v.14 n.1, p.69-111, January 2004 [doi>10.1017/S0956796803004829]
• 11: Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. Technical Report CMU--CS--FOX--95--05, Carnegie Mellon University, 1995.
• 12: J. Strother Moore, A mechanically verified language implementation, Journal of Automated Reasoning, v.5 n.4, p.461-492, Dec. 1989
• 13: Andrew McCreight , Zhong Shao , Chunxiao Lin , Long Li, A general framework for certifying garbage collectors and their mutators, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 14: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 15: F. Pfenning , C. Elliot, Higher-order abstract syntax, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.199-208, June 20-24, 1988, Atlanta, Georgia, United States
• 16: G. D. Plotkin. Lambda-definability and logical relations. Memorandum SAI-RM-4, University of Edinburgh, 1973.
• 17: Gordon D. Plotkin. Call-by-name, call-by-value, and the lambda calculus. Theoretical Computer Science, 1:125--159, 1975.
• 18: Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
• 19: Emir PašaliΕ , Walid Taha , Tim Sheard, Tagless staged interpreters for typed languages, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.218-229, October 04-06, 2002, Pittsburgh, PA, USA
• 20: Tim Sheard, Languages of the future, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA [doi>10.1145/1028664.1028711]
• 21: Matthieu Sozeau. Subset coercions in Coq. In Proc. TYPES, 2006.
• 22: D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.181-192, May 21-24, 1996, Philadelphia, Pennsylvania, United States

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Reliability; Correctness proofs

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Languages, Verification

Keywords:
compiler verification, denotational semantics, dependent types, interactive proof assistants