Biorthogonality, step-indexing and compiler correctness

ABSTRACT

We define logical relations between the denotational semantics of a simply typed functional language with recursion and the operational behaviour of low-level programs in a variant SECD machine. The relations, which are defined using biorthogonality and stepindexing, capture what it means for a piece of low-level code to implement a mathematical, domain-theoretic function and are used to prove correctness of a simple compiler. The results have been formalized in the Coq proof assistant.

REFERENCES

• 1: M. Abadi. TT-closed relations and admissibility. Mathematical Structures in Computer Science, 10(3), 2000.
• 2: M. Abadi. Protection in programming-language translations. In 25th International Colloquium on Automata, Languages and Programming (ICALP), volume 1443 of Lecture Notes in Computer Science, 1998.
• 3: A. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In 15th European Symposium on Programming (ESOP), volume 3924 of Lecture Notes in Computer Science, 2006.
• 4: A. Ahmed and M. Blume. Typed closure conversion preserves observational equivalence. In 13th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2008.
• 5: A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence. In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2009.
• 6: A. Appel and D. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems (TOPLAS), 23(5), 2001.
• 7: A.W. Appel, P.-A. Mellies, C.D. Richards, and J. Vouillon. A Very Modal Model of a Modern, Major, General Type System. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2007.
• 8: N. Benton. Abstracting allocation: The new new thing. In 20th International Workshop on Computer Science Logic (CSL), volume 4207 of LNCS, 2006.
• 9: N. Benton and N. Tabareau. Compiling functional types to relational specifications for low level imperative code. In 4th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI), 2009.
• 10: N. Benton and U. Zarfaty. Formalizing and verifying semantic type soundness of a simple compiler. In 9th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP), 2007.
• 11: N. Benton, A. Kennedy, and C. Varming. Some domain theory and denotational semantics in Coq. In 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 5674 of Lecture Notes in Computer Science, 2009.
• 12: A. Chlipala. A certified type-preserving compiler from lambda calculus to assembly language. In ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI), 2007.
• 13: M. Dave. Compiler verification: a bibliography. ACM SIGSOFT Software Engineering Notes, 28(6), 2003.
• 14: J. Guttman, J. Ramsdell, and M. Wand. VLISP: A verified implementation of scheme. Lisp and Symbolic Computation, 8(1/2), 1995.
• 15: T. Hardin, L. Maranget, and B. Pagano. Functional runtime systems within the lambda-sigma calculus. Journal of Functional Programming, 8, 1998.
• 16: A. Kennedy. Securing the .NET programming model. Theoretical Computer Science, 364(3), 2006.
• 17: J. L. Krivine. Classical logic, storage operators and second-order lambda calculus. Annals of Pure and Applied Logic, 1994.
• 18: P. Landin. The mechanical evaluation of expressions. The Computer Journal, 6(4), 1964.
• 19: X. Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2006.
• 20: X. Leroy and H. Grall. Coinductive big-step operational semantics. Information and Computation, 207(2), 2009.
• 21: J. Longley. When is a functional program not a functional program? In 4th ACM SIGPLAN International Conference on Functional Programming (ICFP), 1999.
• 22: J. McCarthy and J. Painter. Correctness of a Compiler for Arithmetic Expressions. Proceedings Symposium in Applied Mathematics, 19:33--41, 1967.
• 23: A. M. Pitts and I. D. B. Stark. Operational reasoning for functions with local state. In Higher Order Operational Techniques in Semantics. CUP, 1998.
• 24: G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5, 1977.
• 25: J. Vouillon and P.-A. Melli`es. Semantic types: A fresh look at the ideal model for types. In 31st ACM Symposium on Principles of Programming Languages (POPL), 2004.
• 26: G.Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs; Formal methods
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics; Denotational semantics

General Terms:
Languages, Theory, Verification

Keywords:
biorthogonality, compiler verification, denotational semantics, proof assistants, step-indexing