Compiling functional types to relational specifications for low level imperative code

ABSTRACT

We describe a semantic type soundness result, formalized in the Coq proof assistant, for a compiler from a simple functional language into an idealized assembly language. Types in the high-level language are interpreted as binary relations, built using both second-order quantification and separation, over stores and values in the low-level machine.

REFERENCES

• 1: Amal Jamil Ahmed, Semantics of types for mutable state, Princeton University, Princeton, NJ, 2004
• 2: Amal Ahmed , Matthias Blume, Typed closure conversion preserves observational equivalence, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, September 20-28, 2008, Victoria, BC, Canada
• 3: Amal Ahmed , Derek Dreyer , Andreas Rossberg, State-dependent representation independence, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
• 4: Andrew W. Appel, Foundational Proof-Carrying Code, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.247, June 16-19, 2001
• 5: Andrew W. Appel , David McAllester, An indexed model of recursive types for foundational proof-carrying code, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.5, p.657-683, September 2001 [doi>10.1145/504709.504712]
• 6: Andrew W. Appel , Paul-André Melliès , Christopher D. Richards , Jérôme Vouillon, A very modal model of a modern, major, general type system, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 7: N. Benton. Abstracting allocation: The new new thing. In CSL '06, volume 4207 of LNCS. Springer-Verlag, September 2006.
• 8: N. Benton and B. Leperchey. Relational reasoning in a nominal semantics for storage. In Proc. 7th International Conference on Typed Lambda Calculi and Applications (TLCA), volume 3461 of Lecture Notes in Computer Science, 2005.
• 9: Nick Benton , Uri Zarfaty, Formalizing and verifying semantic type soundness of a simple compiler, Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming, July 14-16, 2007, Wroclaw, Poland [doi>10.1145/1273920.1273922]
• 10: Adam Chlipala, A certified type-preserving compiler from lambda calculus to assembly language, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 11: Maulik A. Dave, Compiler verification: a bibliography, ACM SIGSOFT Software Engineering Notes, v.28 n.6, November 2003 [doi>10.1145/966221.966235]
• 12: Rowan Davies , Frank Pfenning, Intersection types and computational effects, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.198-208, September 2000
• 13: N. Glew. Object closure conversion. In 3rd International Workshop on Higher Order Operational Techniques in Semantics, 1999.
• 14: 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
• 15: J. McCarthy and J. Painter. Correctness of a Compiler for Arithmetic Expressions. Proceedings Symposium in Applied Mathematics, 19:33--41, 1967.
• 16: 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]
• 17: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
• 18: Zhaozhong Ni , Zhong Shao, Certified assembly programming with embedded code pointers, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.320-333, January 11-13, 2006, Charleston, South Carolina, USA
• 19: A. M. Pitts , I. D. B. Stark, Operational reasoning for functions with local state, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 20: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 21: N. Tabareau. Modalités de Ressource et Contrôle en Logique Tensorielle. PhD thesis, Université Paris Diderot (Paris 7), 2008.
• 22: G. Tan, A. Appel, K. Swadi, and D. Wu. Construction of a semantic model for a typed assembly language. In Proc. 5th Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '04), 2004.
• 23: Jerome Vouillon , Paul-André Melliès, Semantic types: a fresh look at the ideal model for types, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.52-63, January 14-16, 2004, Venice, Italy
• 24: Hongseok Yang, Relational separation logic, Theoretical Computer Science, v.375 n.1-3, p.308-334, April, 2007 [doi>10.1016/j.tcs.2006.12.036]
• 25: Dachuan Yu , Nadeem A. Hamid , Zhong Shao, Building certified libraries for PCC: dynamic storage allocation, Science of Computer Programming, v.50 n.1-3, p.101-127, March 2004 [doi>10.1016/j.scico.2004.01.003]

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:
  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.3 Studies of Program Constructs
          Subjects: Type structure; Functional constructs

General Terms:
Languages, Theory, Verification

Keywords:
compiler verification, proof assistants, relational parametricity, separation logic, type soundness