Take a look at the new version of this page: [ beta version ]. Tell us what you think.

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: Martín Abadi, ⊤⊤-closed relations and admissibility, Mathematical Structures in Computer Science, v.10 n.3, p.313-320, June 2000 [doi>10.1017/S0960129500003054]
• 2: Martín Abadi, Protection in Programming-Language Translations, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.868-883, July 13-17, 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: 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
• 5: 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
• 6: 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]
• 7: 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
• 8: N. Benton. Abstracting allocation: The new new thing. In 20th International Workshop on Computer Science Logic (CSL), volume 4207 of LNCS, 2006.
• 9: Nick Benton , Nicolas Tabareau, Compiling functional types to relational specifications for low level imperative code, Proceedings of the 4th international workshop on Types in language design and implementation, January 24-24, 2009, Savannah, GA, USA [doi>10.1145/1481861.1481864]
• 10: 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]
• 11: Nick Benton , Andrew Kennedy , Carsten Varming, Some Domain Theory and Denotational Semantics in Coq, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, August 17-20, 2009, Munich, Germany [doi>10.1007/978-3-642-03359-9_10]
• 12: 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
• 13: Maulik A. Dave, Compiler verification: a bibliography, ACM SIGSOFT Software Engineering Notes, v.28 n.6, November 2003 [doi>10.1145/966221.966235]
• 14: 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]
• 15: Thérèse Hardin , Luc Maranget , Bruno Pagano, Functional runtime systems within the lambda-sigma calculus, Journal of Functional Programming, v.8 n.2, p.131-176, March 1998 [doi>10.1017/S0956796898002986]
• 16: Andrew Kennedy, Securing the .NET programming model, Theoretical Computer Science, v.364 n.3, p.311-317, 8 November 2006 [doi>10.1016/j.tcs.2006.08.014]
• 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: 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
• 20: Xavier Leroy , Hervé Grall, Coinductive big-step operational semantics, Information and Computation, v.207 n.2, p.284-304, February, 2009 [doi>10.1016/j.ic.2007.12.004]
• 21: John Longley, When is a functional program not a functional program?, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.1-7, September 27-29, 1999, Paris, France
• 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 , I. D. B. Stark, Operational reasoning for functions with local state, Higher order operational techniques in semantics, Cambridge University Press, New York, NY, 1999
• 24: G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5, 1977.
• 25: 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
• 26: Glynn Winskel, The formal semantics of programming languages: an introduction, MIT Press, Cambridge, MA, 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